Kani formal verification proofs for elicitation contracts.

This crate contains 291 proof harnesses verifying contract invariants using the Kani model checker's symbolic execution engine.

Architecture

Kani proofs are organized by type category:

• Primitives: strings, integers, floats, chars, bools
• Collections: Vec, HashMap, HashSet, arrays, tuples
• DateTime: chrono, time, jiff DateTime types
• Network: IP addresses, MAC addresses, socket addresses
• External: URLs, UUIDs, regex, paths
• Mechanisms: Contract composition and verification

Running Proofs

# All proofs (291 harnesses)
cargo kani -p elicitation_kani --all-features

# Specific module
cargo kani -p elicitation_kani --harness verify_string_non_empty

# With specific features
cargo kani -p elicitation_kani --features uuid,url

Proof Strategy

For each contract type T, we prove:

1. Construction Safety: T::new(x) succeeds ⟹ invariant holds
2. Invalid Rejection: T::new(x) fails ⟹ invariant violated
3. Accessor Correctness: t.get() returns validated value
4. Unwrap Correctness: t.into_inner() returns validated value

Global Configuration

Run with global unwind bound to prevent memchr infinite loops:

cargo kani -p elicitation_kani --all-features -- --default-unwind 20