Kani: A Model Checker Ensuring Rust Code Correctness Beyond Memory Safety

Kani: A Model Checker for Rust

We introduce Kani, an open-source model checker designed to verify Rust code properties that the compiler cannot catch, such as unsafe operations and runtime panics. By compiling proof harnesses into CBMC, Kani automatically checks safety without user annotations. Our tool extends verification to functional correctness using function contracts, successfully uncovering hidden bugs in industrial projects and scaling to verify thousands of harnesses in the Rust standard library.

"Rust's ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness of unsafe operations, functional correctness, and absence of runtime panics."