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 is an experimental methodology for correct-by-construction application state using formal verification. The questions below cover the most common points of confusion: what the proofs actually cover, where the boundaries are, and how to fit dafny-replay into a real application.
dafny-replay proves that state transitions in the verified kernel cannot violate your domain invariant. Concretely:
  • If you discharge the domain obligations (two lemmas for most kernels), all kernel theorems apply to your domain automatically.
  • Undo/redo cannot corrupt state (Replay kernel).
  • The server state always satisfies the invariant regardless of client behavior (Authority and Multi-Collaboration kernels).
  • Pending actions are never silently lost and retries are bounded (Effect State Machine).
What is not proved: networking, databases, authentication, realtime delivery, or the correctness of your specifications themselves.See the guarantees reference for the full list of theorems, obligations, and integration boundaries for each kernel.
No. dafny-replay is server-authoritative, not peer-to-peer.CRDTs guarantee convergence across replicas without a central authority, typically by weakening semantics (unordered sets, tombstones) to achieve commutativity. dafny-replay takes the opposite approach: a single authoritative server maintains strong global invariants, and clients submit requests that the server accepts or rejects.The Multi-Collaboration kernel handles offline clients and stale versions through intent-relative rebasing — the server tries candidates in order and rejects only when no meaning-preserving interpretation can succeed — but this is reconciliation against an authority, not symmetric convergence.
No. dafny-replay owns state transitions and proofs; React (or any other UI layer) owns rendering and user interaction.The boundary is clean: Dafny-generated code lives in a .cjs bundle you import into JavaScript. You store kernel state in React’s useState, call Dispatch, Undo, and Redo from event handlers, and pass the resulting state to your components as props. dafny-replay has no opinion about your component tree, styling, or routing.
Yes. The Authority kernel is designed for server-authoritative state without local history. Its state space is ServerState = { version, present }, not a History.Use the Authority kernel when:
  • You want server-side safety independent of client correctness.
  • You do not need local undo/redo.
  • Clients may submit optimistic actions, but the server is the sole source of truth.
Use the Replay kernel when you need local undo/redo and time-travel in a single-client setting.
The Multi-Collaboration kernel handles clients that submit actions based on stale server versions.When a stale action arrives, the server:
  1. Rebases the action through the intervening history using the domain-defined Rebase function.
  2. Enumerates a finite set of Candidates in order.
  3. Tries each candidate with TryStep; accepts the first success, or rejects if all fail.
The kernel proves intent-relative minimal rejection: if any candidate within the domain’s declared intent envelope (Explains) would succeed, the request is not rejected. The domain defines the envelope; the kernel guarantees the boundary.For position-sensitive operations like card moves, dafny-replay uses anchor-based placement (Before(anchor), After(anchor), AtEnd) instead of positional indices, which are more robust to concurrent edits.
dafny-replay is not optimized for performance. It is an experimental methodology focused on correctness by construction, not throughput or latency.Specific costs to be aware of:
  • Dafny integers compile to BigNumber objects, which are slower than native JS numbers.
  • Immutable Dafny maps and sequences create new objects on every update.
  • The BigNumber.EUCLID modulo configuration must be set globally before any Dafny code runs.
For small-to-medium application state, the overhead is not noticeable in practice. For high-frequency updates or large data structures, you may need to benchmark and consider whether the correctness guarantees justify the cost.
Yes. dafny-replay includes a backend abstraction layer that separates verified transition logic from I/O.Two reference backend integrations are provided:
BackendFeatures
SupabaseManaged auth (OAuth), Row Level Security, built-in realtime
CloudflareD1, Workers, Durable Objects, custom JWT auth
You can implement your own backend by providing the storage and realtime layers that the effect state machine expects. The verified kernels do not depend on any specific backend.See the backends overview for integration details.
dafny-replay targets a recent stable release of Dafny. Check the repository’s CI configuration (.github/workflows/ci.yml) for the exact version pinned in the test suite — that is the version the proofs are known to pass on.For Dafny installation instructions and release notes, see dafny.org.
dafny-replay doubles as a benchmark for Dafny + LLM proof assistance. The workflow separates human review from LLM implementation:
  1. A human expresses the domain intent in natural language.
  2. An LLM generates a formal Dafny specification (types, invariant, apply function).
  3. The human reviews and approves the spec — this is the only review required.
  4. An LLM writes the implementation lemmas and proofs.
  5. Dafny verifies every implementation against the approved spec.
Because Dafny checks the proofs mechanically, the LLM’s implementations are either correct or rejected by the verifier — human review of implementation code is not required. The trust surface is the specification, which is kept small and human-readable by design.Check out lemmafit, which streamlines this methodology.
app-extras.js is the recommended pattern for customizing the generated API without modifying generated code.The dafny2js tool generates app.js automatically from your Dafny source. Because app.js is regenerated every time you recompile, you should not edit it directly. Instead, create app-extras.js that imports app.js, spreads its exports, and overrides or adds methods:
import GeneratedApp from './app.js';

const App = {
  ...GeneratedApp,

  // Accept plain JS strings instead of Dafny seq<char>
  AddMember: (model, name) => {
    return GeneratedApp.AddMember(model, name); // GeneratedApp handles conversion
  },

  // Simplify a multi-argument function
  MakeExpense: (paidBy, amount, shares) => {
    return GeneratedApp.MakeExpense(paidBy, amount, shares, Object.keys(shares));
  },
};

export default App;
Common use cases: simplifying multi-argument functions, wrapping Result types into { ok, value } objects, providing object-style enum access, and accepting JSON for server communication.See the app-extras pattern guide for a complete walkthrough.

Guarantees reference

Full list of kernel theorems, domain obligations, and integration boundaries.

Type mappings reference

Every Dafny-to-JavaScript type conversion with copy-paste examples.

Build docs developers (and LLMs) love

Get started for freeTalk to us