Expand description
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
Modules§
- bools
- Verus proofs for boolean contract types.
- chars
- collections
- Verus proofs for collection contract types.
- datetimes
- durations
- external_
types - floats
- integers
- ipaddr_
bytes - macaddr
- networks
- pathbytes
- paths
- primitives
- regexbytes
- regexes
- serde_
boundary - socketaddr
- stdlib_
collections - strings
- tuples
- urlbytes
- urls
- utf8
- uuid_
bytes - uuids
- values