Skip to content

Latest commit

 

History

History
69 lines (60 loc) · 2.64 KB

KANI.md

File metadata and controls

69 lines (60 loc) · 2.64 KB
Raw

Kani

This document describes how to locally install and use Kani, along with its experimental PropProof feature. Because of instability in Kani internals, the GitHub action is the recommended option if you are running in CI.

Kani is a software verification tool that complements testing by proving the absence of certain classes of bugs like unwrap exceptions, overflows, and assertion failures. See the Kani book for a full list of capabilities and limitations.

Installing Kani and PropProof

  • The install instructions for Kani can be found here. Once Kani is installed, you can run with cargo kani for projects or kani for individual Rust files.

  • [UNSTABLE] To use PropProof, first download the source code from the Kani repository.

    git clone https://github.com/model-checking/kani.git --branch features/proptest propproof
cd propproof; git submodule update --init

    Then, use .cargo/config.toml enable it in the local directory you want to run Kani in. This will override the proptest import in your repo.

    cd $YOUR_REPO_LOCAL_PATH
mkdir '.cargo'
echo "paths =[\"$PATH_TO_PROPPROOF\"]" > .cargo/config.toml

Please Note:

  • features/proptest branch under Kani is likely not the final location for this code. If these instructions stop working, please consult the Kani documentation and file an issue on the Kani repo.
  • The cargo config file will force cargo to always use PropProof. To use proptest, delete the file.

Running Kani

After installing Kani and PropProof, cargo kani --tests should automatically run proptest! harnesses inside your crate. Use --harness to run a specific harness, and -p for a specific sub-crate.

If Kani returns with an error, you can use the concrete playback feature using --enable-unstable --concrete-playback print and paste in the code to your repository. Running this harness with cargo test will replay the input found by Kani that produced this crash. Please note that this feature is unstable and using --concrete-playback inplace to automatically inject a replay harness is not supported when using PropProof.

Debugging CI Failure

      - name: Verify with Kani
        uses: model-checking/[email protected]
        with:
          enable-propproof: true
          args: |
            $KANI_ARGUMENTS

The above GitHub CI workflow is equivalent to cargo kani $KANI_ARGUMENTS with PropProof installed. To replicate issues locally, run cargo kani with the same arguments.