Skip to content

v0.8.2: Compositional Verification Trifecta

Choose a tag to compare

View all tags
@crumplecup crumplecup released this 23 Feb 19:31
· 974 commits to main since this release
v0.8.2
ba4c766

Elicitation v0.8.2: Compositional Verification Trifecta

We're excited to announce Elicitation v0.8.2, marking a major milestone in accessible formal verification for Rust.

🎯 What's New

Three Verifiers, One Derive

For the first time, users can derive formal verification proofs across three major verification tools from a single source:

  • Kani (CBMC-based bounded model checking)
  • Verus (SMT-based executable specifications)
  • Creusot (Rust to Why3 deductive verification)

Simply derive Elicit on your types:

#[derive(Elicit)]
struct MyType {
    validated_field: NonEmptyString,
    count: BoundedU32<1, 100>,
}

Auto-Generated Verification Harnesses

New trait methods generate complete verification harnesses for your custom types:

  • kani_proof() - Generates Kani test harnesses with property checks
  • verus_proof() - Generates Verus specifications with pre/post conditions
  • creusot_proof() - Generates Creusot contracts with invariants

No manual proof writing required. The proofs compose automatically from verified primitives.

🏗️ Compositional Verification

Build formally verified systems from the ground up:

  1. Foundation: All Rust std lib types verified (integers, strings, collections, etc.)
  2. Third-party crates: Popular types like Uuid, Url, Regex verified
  3. Your types: Derive Elicit to inherit verification guarantees
  4. Complex systems: Compose verified types into state machines and protocols

🎓 Real-World Applications

This enables formal verification for:

  • Privacy: Prove data handling guarantees
  • Security: Verify cryptographic protocols and access control
  • Safety: Critical systems requiring certification (aerospace, medical, automotive)

Present formally verified proofs to regulators, auditors, and stakeholders with confidence.

📦 What's Included

  • elicitation - Core derive macro and traits
  • elicitation_kani - Kani verification support (49 proofs verified)
  • elicitation_verus - Verus verification support (49 proofs verified)
  • elicitation_creusot - Creusot verification support
  • elicitation_rand - Property-based testing integration

🚀 Getting Started

[dependencies]
elicitation = "0.8.2"

[dev-dependencies]
elicitation_kani = "0.8.2"
use elicitation::Elicit;

#[derive(Elicit)]
struct UserCredentials {
    username: NonEmptyString,
    password_hash: Bytes<32>,  // Fixed-size verified
}

// Generate verification proofs
#[cfg(kani)]
#[kani::proof]
fn verify_credentials() {
    UserCredentials::kani_proof();
}

Run verification:

cargo kani

📚 Documentation

🙏 Credits

Special thanks to the teams behind Kani, Verus, and Creusot for building these incredible verification tools.

🔮 What's Next

  • Expanded third-party crate coverage
  • Method-level verification (beyond type-level)
  • Interactive proof refinement
  • Performance optimizations

Note: This is a foundational release. While the verification infrastructure is production-ready, we recommend thorough testing for safety-critical applications.

Try it today and experience compositional formal verification in Rust!

Assets 2
Loading