The Kani Rust Verifier is a bit-precise model checker for Rust.

Kani is particularly useful for verifying unsafe code in Rust, where many of the language's usual guarantees are no longer checked by the compiler. Kani verifies:

• Memory safety (e.g., null pointer dereferences)
• User-specified assertions (i.e., assert!(...))
• The absence of panics (e.g., unwrap() on None values)
• The absence of some types of unexpected behavior (e.g., arithmetic overflows)

To install the latest version of Kani (Rust 1.58+; Linux or Mac), run:

cargo install --locked kani-verifier
cargo kani setup

See the installation guide for more details.

Similar to testing, you write a harness, but with Kani you can check all possible values using kani::any():

use my_crate::{function_under_test, meets_specification, precondition};

#[kani::proof]
fn check_my_property() {
   // Create a nondeterministic input
   let input = kani::any();

   // Constrain it according to the function's precondition
   kani::assume(precondition(input));

   // Call the function under verification
   let output = function_under_test(input);

   // Check that it meets the specification
   assert!(meets_specification(input, output));
}

Kani will then try to prove that all valid inputs produce acceptable outputs, without panicking or executing unexpected behavior. Otherwise Kani will generate a trace that points to the failure. We recommend following the tutorial to learn more about how to use Kani.

Use Kani in your CI with model-checking/kani-github-action@VERSION. See the GitHub Action section in the Kani book for details.

See SECURITY for more information.

If you are interested in contributing to Kani, please take a look at the developer documentation.

Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0).

See LICENSE-APACHE and LICENSE-MIT for details.

Kani contains code from the Rust project. Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.

See the Rust repository for details.