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
- clap_
types - collections
- Verus proofs for collection contract types.
- datetimes
- durations
- egui_
types - external_
types - floats
- gallery
- Verus proof gallery — learning curriculum for the VSM companion pattern.
- generated
- Generated VSM companion proofs — produced by
elicitation generate verus. - geo_
types - geojson_
types - georaster_
types - integers
- ipaddr_
bytes - macaddr
- networks
- palette_
types - pathbytes
- paths
- primitives
- proj_
types - ratatui_
types - regexbytes
- regexes
- rstar_
types - serde_
boundary - socketaddr
- sqlx_
types - stdlib_
collections - strings
- tokio_
types - tuples
- ui_
types - urlbytes
- urls
- utf8
- uuid_
bytes - uuids
- values
- wgpu_
types - winit_
types - wkb_
types - wkt_
types