Kani model checker for Rust catches bugs the compiler misses

Kani is an open-source model checker for Rust developed by researchers at Amazon (Rémi Delmas, Zyad Hassan, Qinheping Hu, and others) in collaboration with academia. It addresses a critical gap: while Rust's ownership system prevents memory errors in safe code, it cannot guarantee correctness of unsafe operations (e.g., raw pointer dereferences), functional correctness, or absence of runtime panics. Kani performs bounded model checking by compiling proof harnesses from Rust's Mid-level Intermediate Representation (MIR) into CBMC's bit-precise verification engine. This enables automatic checking of a comprehensive set of safety properties without any user annotation. For unbounded verification, Kani provides a specification language with function contracts, loop contracts, quantifiers, and function stubbing.

In case studies on real-world industrial Rust projects, Kani's contract-based approach upgraded verification from mere panic-freedom to full functional correctness, uncovering six previously unknown bugs. The tool is already operating at scale in production continuous integration (CI): the Rust standard library verification campaign uses over 16,000 harnesses per code change. Accepted at the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2026), Kani represents a practical leap in formal verification for Rust, enabling developers to catch subtle correctness issues that escape the compiler's type system.