dafny-replay provides a set of reusable, formally verified kernels for application state management. Write your domain logic in Dafny, prove its invariants once, and compile to JavaScript for use in React. Every state transition — including undo/redo and collaborative reconciliation — is mathematically guaranteed to preserve your invariants.Documentation Index
Fetch the complete documentation index at: https://mintlify.com/metareflection/dafny-replay/llms.txt
Use this file to discover all available pages before exploring further.
Quickstart
Build a verified React app in 10 steps with a working counter example.
Kernels overview
Explore the five generic kernels: Replay, Authority, Multi-Collaboration, Effect State Machine, and Multi-Project.
Domain obligations
Learn the two proofs you must write to plug your domain into any kernel.
dafny2js tool
Generate JavaScript integration layers automatically from your Dafny code.
How it works
dafny-replay separates concerns cleanly: Dafny owns state transitions and proofs, React owns rendering and user interaction.Define your domain in Dafny
Write a
Model type, Action datatype, Inv predicate, and Apply function. Prove two lemmas: that the initial state satisfies the invariant, and that every transition preserves it.Plug into a kernel
Refine one of the generic kernels (Replay, Authority, MultiCollaboration) with your domain. The kernel’s theorems — undo/redo correctness, minimal rejection, bounded retries — automatically apply to your domain.
Compile to JavaScript
Run
dafny translate js to compile your verified Dafny code to a .cjs bundle, then use dafny2js to generate a clean JavaScript API wrapper.The kernel lineup
Replay kernel
Local undo/redo with time-travel. Proved once: Do, Undo, and Redo cannot violate your domain invariant.
Authority kernel
Server-authoritative state with optimistic clients. Server safety is independent of client correctness.
Multi-Collaboration kernel
Offline-first collaboration with anchor-based reconciliation and intent-relative minimal rejection.
Effect State Machine
Client-side effect orchestration with bounded retries, FIFO processing, and no silent data loss.
Multi-Project kernel
Cross-project operations (MoveTaskTo, CopyTaskTo) with per-project invariant preservation.
Guarantees reference
Precise statement of what is proved, what is assumed, and what is trusted.
Example apps
The repository includes fully verified applications demonstrating the kernels on realistic domains.Kanban board
Exact card partition, WIP limits, drag-and-drop undo/redo.
CollabTodo
Collaborative task lists with cross-project move/copy operations.
ClearSplit
Expense splitting with mathematically guaranteed conservation of money.
ColorWheel
Color palette generator with mood and harmony constraint proofs.
Canon
Diagram editor with referential integrity and constraint solver.
Counter
Minimal toy example for bootstrapping the pipeline.