Rust still has no support for true formal analysis. It is therefore pointless to use it for high safety. Use a real theorem checker instead.

Now Rust as a target for compiling proofs into a programming language is pretty nice. Safe code can have no aliasing due to borrow checker (which should also be formally verified). Threading issues are vastly simplified, though fairness still has to be verified, as well as a few other properties.