A formally verified partial value constructor for facet.
Trame manages incremental construction of values, tracking which fields have been initialized and ensuring proper cleanup on failure. It's designed to be verified from the ground up.
Trame uses a layered verification approach combining four complementary techniques:
| Approach | Coverage | Speed | Annotation Cost | What it catches |
|---|---|---|---|---|
| Kani + VRuntime | Exhaustive within bounds | Slow (exponential) | None | Logic bugs, invariant violations |
| Proptest + VRuntime | Statistical | Fast | None | Logic bugs via random exploration |
| AFL + LRuntime | Statistical | Fast | None | Memory bugs, crashes, UB |
| Creusot (migration in progress) | Unbounded/Universal | Fast (per-function) | High | Everything, with proof |
The codebase is generic over an IRuntime trait with two active implementations:
- VRuntime (Verified Runtime) - Bounded state for Kani proofs and proptest. Uses fixed-size arrays, fat pointers with allocation tracking, and explicit byte-range initialization tracking. No real memory allocation.
- LRuntime (Live Runtime) - Real memory operations for production use and fuzzing.
Kani exhaustively explores all execution paths within bounds (e.g., up to 8 fields, 2-3 operations). This catches logic bugs fast with zero annotation overhead.
Proofs are run via soteria-rust, a
Kani-compatible symbolic execution engine: just kani in the trame/ directory.
Proptest generates random shapes and operation sequences to exercise VRuntime statistically. This catches logic bugs that fall outside Kani's bounded state space, with no annotation overhead.
Run with cargo nextest run (the trame-proptest crate).
AFL fuzzing exercises LRuntime with real memory allocations, catching memory safety issues and crashes that only manifest with actual allocations.
Run with just fuzz.
CRuntime is retired.
Future Creusot work is expected to resume against the live/verified runtimes directly, instead of maintaining a separate logic-only runtime.
Trame has a work-in-progress spec you can visualize via the tracey web subcommand,
see tracey
CI runs on Depot runners. Thanks to Depot for the sponsorship!
Licensed under either of Apache License, Version 2.0 or MIT license at your option.
