Kani Rust Verifier

Kani is a bit-precise model checker for Rust that proves properties about code rather than just testing examples. Unlike tests that check specific inputs, Kani exhaustively verifies all possible inputs.

Installation

# Install Kani (requires Rust 1.58+, Linux/Mac)
cargo install --locked kani-verifier
cargo kani setup

Core Concepts

Proof Harnesses vs Tests

Tests verify specific examples; Kani harnesses verify all possible inputs:

// Test: checks ONE specific case
#[test]
fn test_abs() {
    assert_eq!(abs(-5), 5);
}

// Kani: checks ALL i32 values
#[cfg(kani)]
#[kani::proof]
fn verify_abs() {
    let x: i32 = kani::any();  // Symbolic: represents ALL i32 values
    let result = abs(x);
    assert!(result >= 0);
}

What Kani Automatically Checks

Without any assertions, Kani automatically verifies:

Memory safety (null dereferences, out-of-bounds)
Arithmetic overflows
Division by zero
Shift overflows
Absence of panics (unwrap() on None, etc.)

Quick Start Pattern

#[cfg(kani)]
mod verification {
    use super::*;

    #[kani::proof]
    fn verify_function() {
        // 1. Create symbolic inputs
        let input: u32 = kani::any();

        // 2. Constrain inputs if needed
        kani::assume(input < 1000);

        // 3. Call function under test
        let result = function_under_test(input);

        // 4. Assert properties
        assert!(result > 0);
    }
}

Run with: cargo kani

Essential API

Symbolic Values

// Create symbolic values for any type implementing kani::Arbitrary
let x: u32 = kani::any();
let opt: Option<i32> = kani::any();
let arr: [u8; 4] = kani::any();

// With constraint
let bounded = kani::any_where(|x: &u32| *x < 100);

Assumptions and Assertions

// Constrain symbolic values (preconditions)
kani::assume(x != 0);           // x cannot be zero
kani::assume(x > 0 && x < 100); // bounded range

// Custom assertions with messages
kani::assert(result > 0, "Result must be positive");

// Standard assert! also works
assert!(value.is_some());

Coverage Checking

// Verify a condition is reachable (catches over-constrained harnesses)
kani::cover!(x > 100, "Large values are possible");

Implementing Arbitrary for Custom Types

// Option 1: Derive macro
#[cfg_attr(kani, derive(kani::Arbitrary))]
struct Point { x: i32, y: i32 }

// Option 2: Manual implementation
#[cfg(kani)]
impl kani::Arbitrary for Rating {
    fn any() -> Self {
        match kani::any::<u8>() % 3 {
            0 => Rating::Low,
            1 => Rating::Medium,
            _ => Rating::High,
        }
    }
}

Function Contracts (Experimental)

Contracts enable modular verification with requires (preconditions) and ensures (postconditions):

#[cfg_attr(kani, kani::requires(divisor != 0))]
#[cfg_attr(kani, kani::ensures(|result: &u32| *result <= dividend))]
fn safe_div(dividend: u32, divisor: u32) -> u32 {
    dividend / divisor
}

#[cfg(kani)]
mod verification {
    use super::*;

    #[kani::proof_for_contract(safe_div)]
    fn check_safe_div() {
        let a: u32 = kani::any();
        let b: u32 = kani::any();
        safe_div(a, b);  // Kani verifies contract holds
    }
}

Enable with: cargo kani -Z function-contracts

Handling Loops

Kani must unwind loops to a finite bound:

#[kani::proof]
#[kani::unwind(11)]  // Unwind up to 11 iterations
fn verify_loop() {
    let mut sum = 0u32;
    for i in 0..10 {
        sum = sum.saturating_add(i);
    }
    assert!(sum == 45);
}

Global default: cargo kani --default-unwind 10

Stubbing Functions

Replace complex functions with simpler models:

fn my_random() -> u32 {
    kani::any()  // Return symbolic value instead of actual random
}

#[kani::proof]
#[kani::stub(rand::random, my_random)]
fn verify_with_random() {
    let x = rand::random::<u32>();
    // Verification continues with symbolic x
}

Common Patterns

Verifying Data Structure Invariants

#[kani::proof]
fn verify_vec_push() {
    let mut v: Vec<u32> = kani::any();
    kani::assume(v.len() < 10);

    let old_len = v.len();
    v.push(kani::any());

    assert!(v.len() == old_len + 1);
}

Verifying Unsafe Code

#[kani::proof]
fn verify_raw_pointer() {
    let x: u32 = kani::any();
    let ptr = &x as *const u32;

    // Kani checks this dereference is safe
    let value = unsafe { *ptr };
    assert!(value == x);
}

Bounded Verification

#[kani::proof]
#[kani::unwind(5)]
fn verify_bounded_slice() {
    let data: [u8; 4] = kani::any();
    let idx: usize = kani::any();
    kani::assume(idx < data.len());

    let _ = data[idx];  // Kani proves no out-of-bounds
}

Cargo.toml Configuration

[package.metadata.kani.flags]
default-unwind = "10"

[lints.rust]
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

Command Reference

cargo kani                        # Verify all harnesses
cargo kani --harness verify_foo   # Single harness
cargo kani --tests                # Include test mode dependencies
cargo kani --default-unwind 20    # Set loop bound
cargo kani -Z function-contracts  # Enable contracts
cargo kani --concrete-playback=print  # Generate failing test case

Interpreting Results

VERIFICATION:- SUCCESSFUL    # Property holds for ALL inputs
VERIFICATION:- FAILED        # Counterexample found
Status: UNREACHABLE          # Code path impossible (may indicate over-constrained assume)

Limitations

No concurrency support
No inline assembly
Some floating-point operations are over-approximated
Stack unwinding not supported (use panic = "abort")

References

Full documentation: https://model-checking.github.io/kani/
GitHub: https://github.com/model-checking/kani
API reference: See references/API.md in this skill