tools-verify-kani

Goal

Formally verify a Rust component using Kani. Kani proves absence of panics, arithmetic overflows, and invariant violations for all possible inputs — not just sampled ones. The output is either a passing proof or a concrete counterexample pointing to a real bug.

Work on a dedicated branch (e.g. kani_harnesses) so harnesses and fixes can be reviewed separately from feature work.

The core rule — verify at function granularity, against a spec-derived contract

Before anything else: the unit of verification is a whole function plus a property from the spec — never a cherry-picked statement. Lifting a suspect line and checking it for overflow/out-of-bounds is bug-hunting: it proves a fragment that has no contract, so a green result only says "this one line does not panic." Instead, for each target produce three things and label the global Pn:

precondition — kani::assume(...) the spec's precondition (mirror the production guard);
function — call the real function (preferred: the proof then tracks shipped code). A faithful whole-function copy carrying the same contract is acceptable only where the crate cannot be built under Kani, and must carry a drift/equality check;
postcondition — assert!(...) the spec's postcondition.

Then validate the harness by fault injection: make a change to the function that violates the contract and confirm the harness fails. If it still passes, the harness is not bound to the real code — fix it. (--harness substring-matches; use --exact with the fully-qualified module::name to run one harness in isolation.)

The statement scan in Phase 1 is only for finding candidate functions and their properties — not for lifting statements into harnesses.

Phase 1 — Reconnaissance

Before writing a single line of Kani code, read:

All source files: src/lib.rs, src/state.rs, src/entry.rs, and any submodules.
The component's interface file (components/interfaces/src/ixxx.rs).
Cargo.toml — note feature flags, optional deps, and workspace deps.

Build a target list — scan for every arithmetic expression that can panic or wrap:

Pattern	Risk	Example
`x += 1` on integer field	Overflow if field reaches MAX	`read_ref += 1`
`x -= 1` on integer field	Underflow if field is 0	`read_ref -= 1`
`a * b` before a bounds check	Overflow before guard runs	`block_id * BLOCK_SIZE`
`a + b`	Overflow	`offset + BLOCK_SIZE`
`x as usize` widening cast	Safe on 64-bit, not on 32-bit	`size as usize * 4096`
`buf[i]` inside a loop	Out-of-bounds if bound is wrong	`buf[i] = 1`

Also note:

Types with raw pointers or FFI calls → need stubs (Phase 2)
Component framework macros (define_component!) → bypass in harnesses (Phase 3)
Mutex / Condvar / Arc → test the inner state directly, not through locks

Phase 2 — Stub Unsafe / FFI Dependencies

Kani cannot model raw pointers or calls into C/SPDK FFI. Any type that contains these must be replaced with a safe equivalent under #[cfg(kani)].

Rule: Gate the real implementation with #[cfg(not(kani))] and provide a #[cfg(kani)] stub with the identical public API but backed by safe Rust.

// Production struct — raw pointer, FFI deallocator
#[cfg(not(kani))]
pub struct DmaBuffer {
    ptr: *mut std::ffi::c_void,
    len: usize,
    free_fn: unsafe extern "C" fn(*mut std::ffi::c_void),
}

// Kani stub — Vec<u8>, no raw pointers, Drop is a no-op
#[cfg(kani)]
pub struct DmaBuffer {
    data: Vec<u8>,
}

Apply #[cfg(not(kani))] / #[cfg(kani)] to every impl block for the type (Drop, Deref, DerefMut, Debug, Send, Sync, method impls).

Stub rules:

new(size, ...) → vec![0u8; size], no FFI calls
from_raw(ptr, len, ...) → vec![0u8; len], ignore the raw pointer
as_ptr() → self.data.as_ptr() as *mut _ (safe to return, just not deref'd)
Drop → empty body; Vec handles deallocation
Keep unsafe impl Send / unsafe impl Sync — still needed for Arc<T>

Suppress the lint in every affected Cargo.toml:

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

Phase 3 — Write Harnesses

Place all harnesses in a single #[cfg(kani)] mod verification block inside src/lib.rs. This keeps them invisible to cargo build and cargo test.

#[cfg(kani)]
mod verification {
    use super::*;
    // access pub(crate) state types directly from here

    #[kani::proof]
    #[kani::unwind(N)]   // N = deepest loop bound + 1
    fn verify_something() { ... }
}

Harness rules

Use kani::any() for every input — this tells Kani to consider all possible values, not just a sample.

let count: u32 = kani::any();
let key: u64 = kani::any();

Use kani::assume() only for pre-conditions that production code enforces. Every assume is a hypothesis — it must be audited in Phase 4.

kani::assume(count > 0); // only if production code checks count > 0 first

Bypass the component framework. Do not try to drive IFoo through define_component!. Construct the inner state structs (Inner, State, Entry) directly — they are pub(crate) and visible inside mod verification.

let entry = DispatchEntry { read_ref: kani::any(), write_ref: 0, ... };

Avoid heap allocation in harnesses. HashMap::new(), Vec::new(), String::new() pull in __rust_alloc_error_handler which Kani does not support. Instead, test invariants directly on struct fields.

// Bad — HashMap triggers unsupported alloc error handler
let mut map = HashMap::new();
map.insert(key, entry);

// Good — test the guard logic on the struct directly
let active = entry.read_ref > 0 || entry.write_ref > 0;
kani::assert(!active || ..., "...");

Set #[kani::unwind(N)] correctly.

For a loop with bound B: use N = B + 1
For harnesses with no loops: use N = 1
Kani will fail with an unwind error if N is too small

Standard harnesses to write for any component

Harness	What to verify
`verify_increment_no_overflow`	Every `field += 1` site: `checked_add` returns correct value below MAX, `None` at MAX
`verify_decrement_underflow_guarded`	Every `field -= 1` site: safe because production guard `field > 0` exists
`verify_multiplication_no_overflow`	Every `a * b` before a bounds check
`verify_cast_no_overflow`	Every `x as usize * N` on a 32/64-bit sensitive target
`verify_state_invariant`	After a state transition, assert the resulting field values are consistent
`verify_removal_requires_zero_refs`	Entry is only removed when all reference counts are zero
`verify_symmetric_operation`	e.g. acquire then release leaves state identical to before

Phase 4 — The Assume Audit (Critical Step)

After all harnesses pass, audit every kani::assume against the production code. This is the most important step — a passing harness with an unmatched assume only proves safety in a restricted universe.

For each kani::assume(X) in a harness:

Find the corresponding guard in the production code.
If the guard exists → the assume is justified. Leave it.
If no guard exists → the assume is hiding a bug. The production code depends on X being true but never checks it. This is a defect.

Example of a matched assume (safe):

// Harness
kani::assume(entry.read_ref > 0);
// Production code — guard IS present
if entry.read_ref == 0 {
    return Err(DispatchMapError::RefCountUnderflow(key));
}
entry.read_ref -= 1;

Example of an unmatched assume (bug):

// Harness
kani::assume(read_ref < u32::MAX);  // assumed, but...
// Production code — NO guard
entry.read_ref += 1;                // bare increment, can overflow at u32::MAX

Symmetric pairs are a strong signal. If an error enum has Underflow but no Overflow, look for increment sites that lack the matching guard.

Phase 5 — Fix and Re-Verify

Fix pattern for arithmetic overflow

Replace bare arithmetic with checked_* operations and propagate via ?:

// Before
entry.read_ref += 1;

// After
entry.read_ref = entry
    .read_ref
    .checked_add(1)
    .ok_or(ComponentError::RefCountOverflow(key))?;

Apply the same pattern for:

checked_mul — for multiplications before bounds checks
checked_add — for additions (offset + size, etc.)
checked_sub — only if the existing guard can be removed

Add symmetric error variants

When adding an overflow error, add it to the interface error enum (e.g. components/interfaces/src/ixxx.rs) with a symmetric name:

/// Reference count underflow (release when already zero).
RefCountUnderflow(CacheKey),
/// Reference count overflow (acquire when already at u32::MAX).
RefCountOverflow(CacheKey),   // ← add this

Add the matching Display arm.

Tighten the harnesses after fixing

Remove kani::assume calls that were masking the bug. The harness should now verify the full range including the previously-hidden edge case:

// Before fix — assume hid the overflow
kani::assume(read_ref < u32::MAX);
entry.read_ref += 1;

// After fix — no assume needed; checked_add handles all u32 values
let result = entry.read_ref.checked_add(1);
if let Some(r) = result {
    kani::assert(r == entry.read_ref + 1, "...");
} else {
    kani::assert(entry.read_ref == u32::MAX, "overflow only at MAX");
}

Re-run and confirm

cargo kani --manifest-path components/<name>/vN/Cargo.toml

Target: 0 of N failed, all harnesses in Manual Harness Summary show success.

Phase 6 — Document and Commit

Create VERIFICATION.md in the component directory covering:

Component overview and what was verified
The stub approach (if FFI types were involved)
Each harness and what it proves
Bugs found (file, line, expression)
Fixes applied
Final verification output

Commit on the kani_harnesses branch:

git add components/<name>/... components/interfaces/...
git commit -m "Add Kani harnesses for <component>; fix <N> arithmetic gaps"

Common Pitfalls

Pitfall	Symptom	Fix
`HashMap` / `Vec` in harness	`__rust_alloc_error_handler not supported`	Test struct fields directly
`define_component!` wrapper	Complex macro expansion confuses Kani	Construct inner state structs directly
`#[cfg(feature = "X")]` gate	Kani sees wrong version of a type	Check `Cargo.toml` features; pass `--features X` to `cargo kani`
Unwind too low	`unwinding assertion failure`	Increase `#[kani::unwind(N)]` by 1 and retry
`kani::assume` not audited	Harness passes but bug still present	Do Phase 4 audit before declaring success
Stub missing an `impl` block	Compile error under `cargo kani`	Add `#[cfg(kani)]` version of every `impl` for the stubbed type
`write_ref` vs `read_ref` risk	`write_ref` is assign (0/1), not increment — lower risk	Focus overflow checks on fields that are genuinely incremented

Quick Reference

# Run all harnesses in a component
cargo kani --manifest-path components/<name>/vN/Cargo.toml

# Run a single harness
cargo kani --manifest-path components/<name>/vN/Cargo.toml \
  --harness verification::<harness_name>

# Run with a specific feature enabled
cargo kani --manifest-path components/<name>/vN/Cargo.toml \
  --features spdk