You're viewing the readable version of this site. The interactive extras (search, diagrams, read-aloud) need JavaScript and a current browser. Enable JavaScript; if it is already enabled, update your browser.

Learn · All the Ways It Can Break

growing

A Harness Turns Values Symbolic

One proof harness can stand for every value of a finite machine type.

formal-methods, kani, rust, bounded-model-checking, integer-overflow, learn

You will install Kani 0.67.0, create a proof harness, distinguish symbolic choice from random sampling, reproduce an overflow counterexample, and prove the repaired midpoint over all ordered u8 inputs.

Install and set up the verifier

Begin with a blank Rust library, then install the pinned public release:

cargo new numeric-proof --lib
cd numeric-proof
cargo install --locked kani-verifier --version 0.67.0
cargo kani setup

The setup command installs the matching verifier components. Keep the Kani version in project documentation or CI; solver and compiler changes are part of the evidence environment.

If cargo kani is not found after installation, ensure Cargo's binary directory is on PATH and confirm with cargo kani --version. If setup or a harness invokes a different release, reinstall the locked 0.67.0 package and rerun cargo kani setup before treating either a failure or success as this chapter's result.

Bounded model checking translates a bounded program execution into logical constraints and searches for a satisfying failure. Kani's getting-started guide covers installation and the first harness.

Keep the negative control

Put the two implementations in src/lib.rs:

rust code/all-the-ways-it-can-break/numeric-kani/numeric.rs#implementations numeric.rs The repaired subtraction is safe only under low <= high; the harness will make that domain explicit.

Then add the paired harnesses:

rust code/all-the-ways-it-can-break/numeric-kani/numeric.rs#symbolic-harnesses numeric.rs kani::any() denotes an arbitrary value of the annotated type. assume retains only ordered pairs.

Run each harness separately:

cargo kani --harness buggy_midpoint_stays_in_range
cargo kani --harness fixed_midpoint_stays_in_range

The first run must report a failed overflow check. The second must report one successfully verified harness. If both are green, the safety checks, harness selection, or broken implementation are not the specimen described here.

Machine arithmetic — predict the failure before asking the solver.

What Kani proved

For the repaired harness, the claim covers every u8 pair satisfying low < high=, the compiled function body, the assertion, and Kani's enabled safety checks. It does not cover a wider integer type, floating-point midpoint, an FFI implementation, disabled checks, or callers that violate the assumed ordering. The machine type makes the value domain finite; loops and allocation introduce separate bounds and costs.

Lessons

  • kani::any() is symbolic choice, not pseudorandom generation.
  • A harness defines both the claim and its input domain.
  • Built-in checks can expose overflow before the user's final assertion fails.
  • A failing control verifies that the proof setup can see the known defect.
  • The verdict applies to compiled machine semantics and declared assumptions.

Practice

  1. Retrieval. How many ordered or unordered u8 pairs exist before assumptions?
  2. Discrimination. Does a successful u8 harness prove the same function for u32?
  3. Transfer. Write paired harnesses for an average of two u16 values, preserving the overflow negative control.

Worked answers

  1. 256 × 256 = 65,536 pairs.
  2. No. The source expression may be similar, but the proof domain and compiled operations differ.
  3. Keep (a + b) / 2 as the failing control and prove a + (b - a) / 2 under a < b= for symbolic u16 inputs.

References

  1. Kani. Getting started. — installation, setup, and proof harnesses
  2. Kani. Kani library reference. — symbolic values, assumptions, assertions, and cover

← Put the Network in the Model Assumptions Spend the Proof Domain →