elicitation_verus

Verus formal verification proofs for elicitation contract types.

This crate contains proof functions for every contract type in the elicitation framework using Verus — a Rust verification tool that uses Z3 as its SMT back-end and supports explicit requires/ensures contracts, executable specifications (spec fn), and ghost variables, all written directly in Rust syntax inside a verus! { … } macro block.

Note: This crate is excluded from the Cargo workspace and requires a separate Verus toolchain installation. It produces no compiled library output — only verification artifacts.

What Verus does

Verus performs unbounded symbolic verification: given a function annotated with a precondition (requires) and a postcondition (ensures), it translates the code to its own VIR (Verus Intermediate Representation), then passes the resulting SMT obligations to Z3. Unlike bounded model checking, this is not limited by loop depth or input size — the proof holds for all mathematically possible inputs satisfying the precondition.

verus! {
    pub fn new(value: i32) -> (result: Result<I32Positive, ValidationError>)
        ensures
            value > 0 ==> (result matches Ok(p) && p.value == value),
            value <= 0 ==> (result matches Err(_)),
    {
        if value > 0 { Ok(I32Positive { value }) }
        else { Err(ValidationError::NotPositive) }
    }
}

Z3 discharges both obligations — the success branch and the failure branch — for every possible i32, giving an unbounded proof of constructor correctness.

Proof patterns

Requires / ensures on constructors

Every contract type has a constructor proof covering both Ok and Err outcomes:

ensures
    value > 0 ==> (result matches Ok(p) && p.value == value),
    value <= 0 ==> (result matches Err(ValidationError::NotPositiveI32(v)) && v == value),

The ==> (implies) combinator lets each branch of the match be stated as a separate logical obligation.

Accessor proofs

Accessor methods carry ensures clauses that tie their return value back to the construction parameter:

pub fn get(&self) -> (result: i32)
    requires self.value > 0,
    ensures  result == self.value,

Ghost state

Some types carry a validated: bool ghost field used purely for proof bookkeeping — it tracks whether the construction contract was satisfied and lets Verus reason about compound types without re-proving sub-contracts:

pub struct VecNonEmpty { pub validated: bool }

pub fn is_validated(&self) -> (result: bool)
    ensures result == self.validated,
{ self.validated }

Compositional proofs

Tuple types compose validation flags with logical conjunction, proving that a pair type is valid exactly when both components are valid:

pub fn is_validated(&self) -> (result: bool)
    ensures result == (self.first_validated && self.second_validated),

Abstraction for external crates

Operations that depend on external crates (regex parsing, UUID construction, IEEE 754 float semantics, Unicode character properties) are abstracted as boolean parameters rather than called directly. We prove the wrapper logic without trying to verify the external library:

// Instead of calling regex::Regex::new(pattern):
pub fn new(compiles: bool) -> (result: Result<RegexValid, ValidationError>)
    ensures
        compiles  ==> (result matches Ok(_)),
        !compiles ==> (result matches Err(_)),

This is the castle on cloud principle applied to Verus: trust the foundations (external crates), verify the walls (our contract logic).

Coverage

Running the proofs

Install Verus following the official instructions, then verify the crate directly:

verus crates/elicitation_verus/src/lib.rs

Verus writes intermediate files to a .verus-log/ directory:

• .vir / -sst.vir — Verus Intermediate Representation
• .air / -final.air — Anvil IR passed to Z3
• .smt2 — SMT-LIB2 queries sent to the solver
• .smt_transcript — Z3 interaction log

For failed proofs, .interp files contain counterexample models from Z3.

Integration with the elicitation crate

elicitation_verus depends on the main elicitation crate with the verification feature enabled:

[dependencies]
elicitation = { version = "0.8", features = ["verification"] }

The main crate defines the contract types; this crate proves their constructors and accessors are correct. Because verification produces no compiled output, there is zero runtime overhead — the proofs exist solely as logical witnesses.

The crate is excluded from the workspace (exclude = [...] in the root Cargo.toml) because it requires Verus's own modified Rust toolchain and cannot be built with standard cargo.

Verus vs. Kani vs. Creusot

The elicitation workspace maintains three independent formal verification back-ends. They address different points on the verification spectrum:

Verus is the natural choice when you need to express rich logical properties — implications, conjunctions over compound types, conditional postconditions — and want a single self-contained toolchain (no Why3 ecosystem required). Kani is faster for concrete numeric/bit properties. Creusot shines for loop-heavy algorithms.

A property proved by all three tools independently has been checked by three completely separate verification paths, providing very high confidence.

License

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