Crate elicitation_kani 

Kani formal verification proofs for elicitation contracts.

This crate contains 386 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
• Third-party: clap, sqlx, tokio, egui, UI typestate types

Running Proofs

# All proofs (386 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

Modules

contracts

Default contract implementations for primitive types.

harness_helpers

Harness helper utilities for writing Kani proof harnesses.

Macros

kani_arbitrary

Generate a kani::Arbitrary impl for a type with String or Vec fields.

Traits

Contract

Generic contract for formal verification.

WithContract

Extension trait for adding contract verification to elicitation.