I fully expect formally verified C to become the standard for any reasonably critical software. It's astonishing how easy it is to crank out program equivalence proofs these days...
Is there a benefit to formally verified C over formally verified Rust? Maybe platform support?
well you can just have much stronger safety guarantees in a theorem prover than in the rust type system, and C is a much easier thing to embed in a theorem prover than rust.
Rust isn't C. There are plenty of theorem provers that are proc macros. C doesn't have proc macros so that's why you wrap it instead, but there's no need to wrap Rust like that.