Ok, but a formally verified compiler is a very different beast from a high quality compiler. We can realistically hope the Rust compiler team significantly improve the correctness of the compiler, but full formal verification is unlikely.

CompCert is an extremely impressive achievement, and compiles a near-complete subset of standard C. A verified Rust compiler would be an enormous undertaking, and would need a very skilled team. It also wouldn't be worth trying unless the Rust language were very stable, which, if I understand correctly, it isn't.