Installation

Kani offers an easy installation option on three platforms:

x86_64-unknown-linux-gnu (Most Linux distributions)
x86_64-apple-darwin (Intel Mac OS)
aarch64-apple-darwin (Apple Silicon Mac OS)

Other platforms are either not yet supported or require instead that you build from source. To use Kani in your GitHub CI workflows, see GitHub CI Action.

Dependencies

The following must already be installed:

Python version 3.7 or newer and the package installer pip.
Rust 1.58 or newer installed via rustup.
ctags is required for Kani's --visualize option to work correctly. Universal ctags is recommended.

Installing the latest version

To install the latest version of Kani, run:

cargo install --locked kani-verifier
cargo kani setup

This will build and place in ~/.cargo/bin (in a typical environment) the kani and cargo-kani binaries. The second step (cargo kani setup) will download the Kani compiler and other necessary dependencies, and place them under ~/.kani/ by default. A custom path can be specified using the KANI_HOME environment variable.

Installing an older version

cargo install --locked kani-verifier --version <VERSION>
cargo kani setup

Checking your installation

After you've installed Kani, you can try running it by creating a test file:

// File: test.rs
#[kani::proof]
fn main() {
    assert!(1 == 2);
}

Run Kani on the single file:

kani test.rs

You should get a result like this one:

[...]
RESULTS:
Check 1: main.assertion.1
         - Status: FAILURE
         - Description: "assertion failed: 1 == 2"
[...]
VERIFICATION:- FAILED

Fix the test and you should see a result like this one:

[...]
VERIFICATION:- SUCCESSFUL

Next steps

If you're learning Kani for the first time, you may be interested in our tutorial.

The Kani Rust Verifier