Rust's borrow checker prevents memory errors, but it doesn't prove functional correctness, panic-freedom, or compliance with a safety envelope. Where a panic is unacceptable, that requires model checking, not just tests.
A common gap: code is assumed safe because it compiles and passes tests, but no proof exists that a given function can't panic under any input.
Integrating Kani into CI for panic-freedom proofs on critical paths, and z3-based verification for safety-envelope properties where the system controls something physical or high-stakes.
Related real work:
open-source, published on crates.io
last commit 45 days ago · 61 downloads · 1 star
z3-verified runtime shield for a robot control policy, demonstrated on a MuJoCo arm
It means the checker couldn't prove or disprove the property in the time given — a genuinely different, more honest result than a false pass. cargo-vouch reports it explicitly rather than treating it as a pass.
Tests find the bugs you thought to check for. Model checking with Kani explores the input space exhaustively (within bounds) and can prove a class of bugs doesn't exist.
Access to your codebase and a diagnostic call about which paths are safety-critical enough to justify formal proof.