The verification ecosystem for C is the last reason that tool-augmented C is safer than Rust. A Rust-to-C compiler might let Rust leverage that. So, thanks for the tip.
I don't think mrustc speaks the C dialects that are friendly to tool augmented verification currently, FWIW. The focus of that project is from source boot strapping, and support for archs that don't have LLVM backends.
