Kani: A Model Checker for Rust

Kani converts Rust's Mid-level Intermediate Representation (MIR) into CBMC bit-precise verification engine inputs to perform bounded model checking. It validates unsafe code soundness, functional correctness, and panic-freedom using a specification language for loop contracts and quantifiers. The tool scales to production CI, verifying over 16,000 harnesses per change in the Rust standard library.