The Kani Rust Verifier aims to be a bit-precise model-checker for Rust. Kani ensures that unsafe Rust code is actually safe, and verifies that safe Rust code will not panic at runtime.

Until an official release is out, you can read documentation on how to check out and build Kani yourself.

Our documentation covers:

• Comparison with other tools
• Failures that Kani can spot
• Kani's current limitations

You write a proof harness that looks a lot like a test harness, except that you can check all possible values using kani::any():

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

#[kani::proof]
fn check_my_property() {
   let input = kani::any();
   kani::assume(is_valid(input));
   let output = function_under_test(input);
   assert!(meets_specification(input, output));
}

Kani will then prove that all valid inputs will produce acceptable outputs, without panicking or executing undefined behavior. You can learn more about how to use Kani by following the Kani tutorial.

See SECURITY for more information.

See Kani 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 compiler. The rust compiler 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.