elicitation_kani

Kani model-checking proofs for elicitation contract types.

This crate contains 386 proof harnesses that formally verify the correctness of every contract type in the elicitation framework using Kani — a Rust model checker that uses symbolic execution to confirm properties hold for all possible inputs, not just the ones you thought to test.

What Kani does

Kani performs bounded model checking: it symbolically executes your Rust code, treating inputs as unknown values that range over every possible bit pattern. When it encounters an assert!, it asks an SMT solver whether a counterexample exists. If none is found within the unwind bound, the property is proved for all inputs.

#[kani::proof]
fn verify_i32_positive_construction() {
    let value: i32 = kani::any(); // symbolic — represents every i32
    match I32Positive::new(value) {
        Ok(wrapped) => assert!(wrapped.get() > 0),  // invariant holds
        Err(_)      => assert!(value <= 0),          // rejection justified
    }
}

Kani symbolically explores every branch for every possible i32, then confirms the invariant without a single test value being chosen by hand.

The "castle on cloud" pattern

The guiding philosophy is: trust the foundations, verify the walls.

We trust the Rust stdlib, chrono, time, jiff, url, uuid, regex and other battle-tested crates for their own correctness. We verify that our wrapper logic — constructors, accessors, generators — uses those foundations correctly.

  ┌─────────────────────────────────────┐
  │  Our wrappers   ← verified by Kani  │
  ├─────────────────────────────────────┤
  │  stdlib / third-party crates        │  ← trusted
  └─────────────────────────────────────┘

This keeps harnesses fast and focused. We do not re-prove that i32 addition is correct; we prove that I32Positive::new stores the value faithfully and that get() returns it.

What is verified

Every contract type has at least two harnesses:

Coverage by module

Running the proofs

Install Kani following the official instructions, then:

# All 386 harnesses
cargo kani -p elicitation_kani --all-features -- --default-unwind 20

# Feature-specific subset
cargo kani -p elicitation_kani --features uuid,chrono -- --default-unwind 20

# Single harness
cargo kani -p elicitation_kani --harness verify_i32_positive_construction

The --default-unwind 20 bound handles loop-containing types (URL parsing, UTF-8 scanning). Simpler harnesses complete in seconds; the full suite runs in roughly five to ten minutes.

Using this crate for your own types

Add it as a dev-dependency. The harnesses here also serve as templates — copy the pattern for your own contract types:

[dev-dependencies]
elicitation_kani = { version = "0.8" }

use elicitation::verification::types::I32Positive;

#[kani::proof]
fn verify_my_wrapper_preserves_positivity() {
    let raw: i32 = kani::any();
    kani::assume(raw > 0);

    let pos = I32Positive::new(raw).unwrap();
    let doubled = pos.get() * 2;

    // Verify: doubling a positive i32 within safe range stays positive
    kani::assume(raw < i32::MAX / 2);
    assert!(doubled > 0);
}

Kani will symbolically verify this for every i32 in (0, MAX/2).

Kani vs. Creusot vs. Verus

The elicitation workspace maintains three independent formal verification back-ends. They are complementary:

Kani is fastest to get started with and excels at concrete bit-level properties (IP range membership, MAC address bit flags, integer bounds). When the same property is proved by all three tools independently, confidence in correctness is very high.

Feature flags

[features]
default = []
kani       # Enable kani-verifier dependency
chrono     # DateTimeUtc, NaiveDateTime generator proofs
time       # OffsetDateTime generator proofs
jiff       # Timestamp symbolic gate proofs
uuid       # UUID generator and byte-level proofs
url        # URL scheme/authority/byte-level proofs
regex      # Layered regex validation proofs

License

Licensed under either of Apache License 2.0 or MIT License at your option.