[xavxav]

Yea, I think that they're taking the correct approach. For certification reasons formal verification is not necessary or even really desirable, but a core hypothesis in my thesis is that we can lower the exponential factor of formal methods for Rust compared to C. The type system of Rust really helps simplify the work and I hope that Rust can be one the the languages that finally takes FV/FM 'mainstream' (it'll never be an average tool but less niche/expert).

To that end I'm always on the lookout for moderate length program components (100-1kloc) with clear safety properties that need to be verified. The standard fare is datastructures, but I'd love to see if we can expand the applications.