Kani: A Model Checker for Rust
Summary
Kani is an open-source model checker for Rust that extends bounded model checking to verify correctness properties for both safe and unsafe code. It compiles proof harnesses from Rust's MIR into CBMC's bit-precise verification engine, enabling automatic checking of safety properties with no user annotations. The authors show case studies on industrial Rust projects, demonstrating that contracts can upgrade verification from panic-freedom to functional correctness and that Kani scales to production CI with thousands of harnesses.