Undo is a feature. Reversibility is a property.
The checked inverse is sealed before actions land. Anyone can verify the verdict afterwards, offline, without trusting whoever issued it.
| Component | Responsibility | Tech Stack | Status |
|---|---|---|---|
TraceFold Core |
Deterministic approval gate, runtime inverse engine, and CLI | Rust 1.97.1 | Core Engine |
@mahirhir/tracefold |
Air-gapped offline receipt verifier (Zero network calls) | TypeScript / WASM | Published (Apache-2.0) |
gui/ |
Local-first visual inspector over execution traces and checkpoints | Desktop UI | Operational |
lean/ |
117 machine-checked algebraic proofs with 0 sorry assertions |
Lean 4 | Formally Verified |
- Core Engine & CLI:
TraceFold/tracefold— Source code, issue tracker, and discussions. - Instant WASM Verifier:
tracefold.github.io/tracefold/verify.html— Standalone in-tab verification. - Formal Technical Report:
docs/TRACEFOLD_TR.md— Mathematical foundation and error taxonomy. - Direct Research Contact:
mahirohirakawa@glovrex.com· Discord:discord.gg/rtvXqYEQzr
Built by Glovrex · Licensed under Apache-2.0
