[wk_end]

This is about verifying the compiler, not proving any properties of the generated code. Totally orthogonal to Rust's aims, unless the Rust compiler has been formally verified (I don't believe it has).

[strangecasts]

There has been work to verify a subset of Rust's logic - https://plv.mpi-sws.org/rustbelt/popl18/ - but the compiler itself is not verified, no.

[steveklabnik]

It has not.