Kani, an open-source model checker for Rust developed by a twelve-person team including Felipe R. Monteiro and Michael Tautschnig, compiles proof harnesses directly from Rust's Mid-level Intermediate Representation into CBMC's bit-precise verification engine. This architecture automatically checks memory safety, panic freedom, and functional correctness without requiring source annotations — a departure from tools that demand manual proof scaffolding.

The system extends bounded verification to unbounded domains through a specification language supporting function contracts, loop contracts, quantifiers, and function stubbing. In case studies across industrial Rust projects, these contracts elevated verification from basic panic-freedom to full functional correctness, exposing six previously unknown bugs that conventional testing missed.

Kani now runs in production CI at AWS, where the Rust standard library verification campaign executes over 16,000 harnesses per code change. This scale demonstrates that model checking has moved beyond academic prototypes into continuous integration pipelines for critical infrastructure.