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:

  • Rust 1.58 or newer installed via rustup.

Installing the latest version

Installing the latest version of Kani is a two step process.

First, download and build Kani's installer package using:

cargo install --locked kani-verifier

This will build and place in ~/.cargo/bin (in a typical environment) the kani and cargo-kani binaries.

Next, run the installer to download and install the prebuilt binaries as well as supporting libraries and data:

cargo kani setup

The second step 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.