1. Of course it can. My model checks on function contracts and invariants run for every function. If a function fails this contract or invariant, the overall bu

1. Of course it can. My model checks on function contracts and invariants run for every function. If a function fails this contract or invariant, the overall build fails. Does it matter that this is a separate build step than the compilation? Not in practice. Think of the model check step as being a semantic analysis step that happens after the type check and syntax check from the compiler. 2. You're not interested in proving that every program that the compiler accepts will be free of issues. You're interested in whether YOUR program that you write is free of those issues. The Rust compiler CAN'T do this, because the Rust compiler is only looking at a SUBSET of the possible things that you can build model checks against. This is why Kani -- a model checker for Rust -- exists. You can model check unsafe code in Rust, as well as safe code in Rust against user assertions and function contracts that are otherwise not possible to check in vanilla Rust. Model checking isn't just for C, but model checking, as a practical form of formal methods, brings the same and even better safety to C. In fact, with Kani, you can get similar safety in Rust as well. If you like Rust, use it. But, as was the point of my comment, it is possible and practical to get similar safety in C.