Kani is an open-source verification tool that uses automated reasoning to analyze Rust programs. Kani is particularly useful for verifying unsafe code in Rust, where many of the Rust’s usual guarantees are no longer checked by the compiler. Some example properties you can prove with Kani include memory safety properties (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., index out of bounds, panics), and the absence of some types of unexpected behavior (e.g., arithmetic overflows). Kani can also prove custom properties provided in the form of user-specified assertions.
Kani uses proof harnesses to analyze programs. Proof harnesses are similar to test harnesses, especially property-based test harnesses.
Kani is currently under active development. Releases are published here. Major changes to Kani are documented in the RFC Book.
There is support for a fair amount of Rust language features, but not all (e.g., concurrency). Please see Limitations - Rust feature support for a detailed list of supported features.
Kani releases every two weeks. As part of every release, Kani will synchronize with a recent nightly release of Rust, and so is generally up-to-date with the latest Rust language features.
If you encounter issues when using Kani, we encourage you to report them to us.