Kani model checker verifies Rust at industrial scale

Category: Dev tools
Status: confirmed
Sources: arXiv 2607.01504, Kani repository, HN discussion
Summary: A paper submitted 2026-07-01 and accepted to the ASE 2026 industry showcase describes Kani, an open-source model checker that compiles verification harnesses from Rust MIR into the CBMC engine to check memory safety, panic freedom, and functional correctness beyond what the compiler guarantees. The authors report a specification language with function and loop contracts, quantifiers, and function stubbing, six previously unknown bugs found in industrial Rust projects, and more than 16,000 harnesses run per code change in the Rust standard-library verification effort, operating in continuous integration.
Why it matters: Bounded and contract-based verification that runs in CI gives Rust teams a way to check unsafe code and correctness properties the type system does not cover, at a scale already applied to the standard library.