Installing from source code

If you were able to install Kani normally, you do not need to build Kani from source. You probably want to proceed to the Kani tutorial.

Dependencies

In general, the following dependencies are required to build Kani from source.

NOTE: These dependencies may be installed by running the scripts shown below and don't need to be manually installed.

  1. Cargo installed via rustup
  2. CBMC (latest release)
  3. CBMC Viewer (latest release)
  4. Kissat (Release 3.0.0)

Kani has been tested in Ubuntu and macOS platforms.

Install dependencies on Ubuntu

Support is available for Ubuntu 18.04, 20.04 and 22.04. The simplest way to install dependencies (especially if you're using a fresh VM) is following our CI scripts:

# git clone git@github.com:model-checking/kani.git
git clone https://github.com/model-checking/kani.git
cd kani
git submodule update --init
./scripts/setup/ubuntu/install_deps.sh
# If you haven't already (or from https://rustup.rs/):
./scripts/setup/install_rustup.sh
source $HOME/.cargo/env

Install dependencies on macOS

Support is available for macOS 11. You need to have Homebrew installed already.

# git clone git@github.com:model-checking/kani.git
git clone https://github.com/model-checking/kani.git
cd kani
git submodule update --init
./scripts/setup/macos/install_deps.sh
# If you haven't already (or from https://rustup.rs/):
./scripts/setup/install_rustup.sh
source $HOME/.cargo/env

Build and test Kani

Build the Kani package:

cargo build-dev

Then, optionally, run the regression tests:

./scripts/kani-regression.sh

This script has a lot of noisy output, but on a successful run you'll see at the end of the execution:

All Kani regression tests completed successfully.

Adding Kani to your path

To use a locally-built Kani from anywhere, add the Kani scripts to your path:

export PATH=$(pwd)/scripts:$PATH

Next steps

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