trame-runtime 0.1.0

Runtime traits and implementations for trame
Documentation

trame-runtime

Runtime traits and implementations for trame.

Defines the IRuntime, IHeap, IShape, IPtr, and IArena traits that abstract over memory operations, allowing trame's core logic to be verified with multiple backends:

  • LRuntime (Live Runtime) - Real memory operations via std::alloc. Zero-cost in production.
  • VRuntime (Verified Runtime) - Bounded state tracking for Kani model checking. Fixed-size arrays, fat pointers with allocation tracking, explicit byte-range initialization tracking.
  • CRuntime (Creusot Runtime) - Backend for deductive verification with Creusot/Why3.

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.