Kani: Formal verification for Rust reaches production CI and the standard library

Rust’s ownership model eliminates memory errors in safe code, but it says nothing about the correctness of unsafe blocks, whether functions actually behave as intended, or whether code can panic at runtime. Kani, an open-source model checker from a team working on industrial Rust, targets exactly those gaps. It lowers proof harnesses from Rust’s Mid-level Intermediate Representation into CBMC’s bit-precise engine and checks a broad set of safety properties automatically, without requiring developers to annotate their code.

The more interesting contribution is how Kani escapes the usual ceiling of bounded model checking. Rather than only hunting for bugs up to a fixed depth, it adds a specification language — function and loop contracts, quantifiers, and function stubbing — that lets engineers prove properties for unbounded inputs. In case studies on real-world Rust projects, contracts pushed verification past mere panic-freedom into full functional correctness and surfaced six previously unknown bugs.

What makes this more than an academic exercise is scale: Kani runs inside production continuous integration, verifying over 16,000 harnesses on every code change as part of an ongoing campaign to verify the Rust standard library. That positions formal verification as a routine gate in a mainstream systems language rather than a specialist’s tool, and gives the wider ecosystem stronger assurances about the unsafe foundations much of Rust ultimately depends on.