[clarus]

There are some people studying Rust with formal verification. For example in this paper https://plv.mpi-sws.org/rustbelt/rbrlx/paper.pdf However I do not know if the whole language is covered or only a core.

[sanxiyn]

The big gap with RustBelt is that it does not cover traits. This actually does matter: some bugs were missed because they interact with traits.