trame-formal

Formally verified partial value construction.

This crate is built from the ground up with Kani verification in mind. Every operation is designed to be verifiable, with bounded state spaces and explicit invariants.

Design Principles

1. One implementation - Business logic is generic over heap
2. Verified heap - Tracks state, asserts valid transitions, bounded for Kani
3. Real heap - Performs actual memory operations (zero-cost, unbounded)

trame

Formally verified partial value construction for facet.

This is the main crate. It provides the Trame state machine for incremental value construction, the Op type for describing operations, and the Path type for addressing fields within nested structures.

The implementation is generic over an IRuntime trait (defined in trame-runtime), allowing the same business logic to run against both a real heap (LRuntime) and a bounded verification heap (VRuntime).

Sponsors

CI runs on Depot runners. Thanks to Depot for the sponsorship!

License

Licensed under either of Apache License, Version 2.0 or MIT license at your option.