Verus verification proofs for elicitation contract types.
This module contains Verus executable specifications for formal verification. Proofs are simplified stubs focusing on type-level contracts.
Verification Architecture
Complete trenchcoat verification pipeline:
- Contract types: User-facing validated types
- Trenchcoat types: Internal stdlib wrappers
- Stdlib types: Trusted foundation
Usage
These proofs are for verification only and don't affect runtime behavior.
Run with: verus crates/elicitation_verus/src/lib.rs