Kani is a bit-precise model checker for Rust.

If you want to be sure that a class of bugs, such as arithmetic overflow, out-of-bounds access, or undefined behavior in unsafe code, can never occur in your Rust crate, you can use Kani to explore all possible execution paths. Or go further and write a specification of how you expect your functions to behave, and Kani will check whether it holds for all possible inputs. Kani aims to make mechanized proofs easy to use for every Rust developer: write a harness like you would write a test, and Kani checks it over all possible inputs.

Get Started