Skip to main content

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.

dafny-replay turns a simple mathematical insight into a practical tool for web development: if every state transition in your application is proved to preserve an invariant, then every state your app can ever reach satisfies that invariant — including after undo, redo, network reconciliation, or any sequence of user actions. You write the proof once, compile it to JavaScript, and React handles the rest.

​
The core idea

Most application bugs are reachability problems: the app ended up in a state it was never supposed to reach. dafny-replay addresses this at its root by making forbidden states unreachable by construction, not by convention. The formal guarantee is straightforward:
If Inv(Init()) holds and every transition satisfies Inv(m) ⇒ Inv(Normalize(Apply(m, a))), then every state reachable through the system — including via replay or protocol interaction — also satisfies Inv.
You provide these two proofs for your domain. The kernels are proved once, generically, and the theorems about undo/redo correctness, server-side safety, and pending-action preservation lift to your domain automatically.
dafny-replay is an experimental methodology, not a UI framework or CRDT library. It focuses exclusively on correctness of application state transitions.

​
What dafny-replay provides

dafny-replay ships five generic verified kernels, each targeting a different setting. You plug your domain into whichever kernel fits your architecture.

Replay kernel

Local undo/redo with time-travel debugging. Proved once: Do, Undo, and Redo cannot violate your domain invariant regardless of action sequence.

Authority kernel

Server-authoritative state with optimistic clients. Server-side invariant safety holds independent of client correctness or network behavior.

Multi-Collaboration kernel

Offline-first collaboration with anchor-based move semantics, candidate fallback, and intent-relative minimal rejection.

Effect State Machine

Client-side effect orchestration with bounded retries, FIFO processing, and a proof that pending actions are never silently lost.

Multi-Project kernel

Cross-project operations (MoveTaskTo, CopyTaskTo) that preserve per-project invariants while handling concurrent edits from multiple clients.

Guarantees reference

Precise statement of what is proved, what is assumed, and what falls outside the verified boundary.

​
The LLM + Dafny workflow

dafny-replay also serves as a benchmark for AI-assisted formal verification. The methodology reduces the surface area of human review while maintaining mathematical guarantees:
  1. You express intent in natural language — describe the invariants your domain should satisfy.
  2. An LLM generates a formal spec — Dafny types, predicates, and proof obligations.
  3. You review and approve the spec — this is the only human review step required.
  4. An LLM writes implementations — verified automatically against the approved spec.
  5. All accepted code is mathematically guaranteed to satisfy the spec.
The lemmafit tool streamlines this workflow, making it easier to drive the LLM + Dafny cycle on your own domains.
The human’s job shrinks to reviewing a spec — a compact formal description of what the system should do — rather than reviewing the implementation details of how it does it.

​
The Replay kernel in depth

The Replay kernel is the foundation of dafny-replay and the simplest kernel to understand. Its architecture: 
Abstract Domain (spec)
        ↓ refined by
Concrete Domain (Model, Action, Inv, Apply, Normalize)
        ↓ plugged into
Replay Kernel (generic, proved once)
        ↓ compiled to JS
AppCore (React-facing API)
The kernel maintains a three-part history: 
History = { past: seq<Model>, present: Model, future: seq<Model> }
and exposes three operations: Do(action), Undo, and Redo. It is proved generically that all three preserve Inv on every entry in the history — past, present, and future.

​
Domain obligations

To use any kernel, you must discharge two proof obligations for your domain: 
(R1)  Inv(Init())
(R2)  Inv(m) ⇒ Inv(Normalize(Apply(m, a)))
After that, undo/redo correctness is automatic. The kernel’s theorems apply without any additional proof work.

​
What the proofs cover — and what they don’t

Verified transition logic runs inside unverified systems. The proofs apply to the Dafny-generated state machine logic, not to the JavaScript runtime, network layer, database, or authentication system surrounding it.
The boundary is explicit:
VerifiedTrusted (not modeled)
State transition logicJavaScript runtime and Dafny-to-JS compilation
Invariant preservation across Do/Undo/RedoUI wiring and rendering
Server-side safety (Authority kernel)Networking, authentication, authorization
Pending-action preservation (Effect SM)Database persistence and I/O
Bounded retriesEnd-to-end liveness
See Guarantees for a complete statement of what each kernel proves, assumes, and trusts.

​
Next steps

Quickstart

Build a verified React counter app step by step using real code from the repository.

Domain obligations

Learn exactly what you must prove to plug your domain into a kernel.

dafny2js tool

Generate a JavaScript integration layer automatically from your Dafny AppCore module.

Example apps

Explore fully verified applications — from a toy counter to a collaborative Kanban board.

Build docs developers (and LLMs) love

Get started for freeTalk to us