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.