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.

Formal methods are only useful if you know where the proofs end. dafny-replay proves correctness for its verified transition logic, but that logic runs inside larger systems — JavaScript runtimes, databases, networks — that are not modeled. This document draws the line precisely so you can reason about your application’s trust boundary with confidence. Throughout this document:
  • Verified means proved in Dafny.
  • Assumed / obligated means must be proved by each concrete domain to instantiate a kernel.
  • Trusted (integration boundary) means not modeled or proved, even though verified code may execute inside it.

​
Notation

SymbolMeaning
Model, ActionVary by domain
Inv : Model → boolDomain invariant
Init : () → ModelInitial state constructor
Ok(_) / Err(_)Result constructors
History{ past, present, future }
ServerState{ version, present }

​
How to read the guarantees

For each kernel, this document lists:
  1. Domain obligations — properties that each concrete domain must prove to use the kernel.
  2. Kernel theorems — properties proved once by the generic kernel, assuming the obligations.
  3. Integration boundary (trusted) — system-level behavior that is not modeled or proved.
When something appears under “trusted,” it does not mean that the Dafny-generated logic inside it is unverified — only that the end-to-end system behavior of that component is not proved.

​
Replay kernel

State space: History over Model

​
Domain obligations

Each domain must prove:
  • (R1) Inv(Init())
  • (R2) Inv(m) ⇒ Inv(Normalize(Apply(m, a)))

​
Kernel theorems

Assuming (R1–R2):
  • (RK1) For all reachable histories h, Inv(Present(h)) holds.
  • (RK2) Do, Undo, and Redo preserve Inv on the present state.
Undo/redo and time travel cannot violate the invariant once the domain obligations are discharged.

​
Integration boundary (trusted)

  • JavaScript runtime and Dafny → JS compilation
  • UI wiring and rendering
  • Persistence, serialization, and I/O

​
Authority kernel

State space: ServerState = { version, present }

​
Domain obligations

Each domain must prove:
  • (A1) Inv(Init())
  • (A2) Inv(m) ∧ TryStep(m, a) = Ok(m′) ⇒ Inv(m′)

​
Kernel theorems

Assuming (A1–A2):
  • (AK1) For any protocol trace (arbitrary client behavior), the authoritative server state always satisfies Inv.
  • (AK2) Rejected requests leave server state unchanged.
The kernel proves server-side safety independent of client correctness.

​
Integration boundary (trusted)

  • Networking, authentication, authorization
  • Database persistence
  • Concurrency beyond the modeled protocol
  • JS/edge wiring

​
Multi-Collaboration kernel

State space: server-authoritative model + operation log + client state

​
Domain obligations

Each domain must provide and prove:
  • (MC1) Inv(Init())
  • (MC2) Inv(m) ∧ TryStep(m, a) = Ok(m′) ⇒ Inv(m′)
  • (MC3) Total rebasing and candidate interface: Rebase, Candidates, Explains, CandidatesComplete

​
Kernel theorems

Assuming (MC1–MC3):
  • (MCK1) Safety: all accepted server states satisfy Inv.
  • (MCK2) Intent-relative minimal rejection: if a request is rejected, then there exists no action aGood such that Explains(rebased, aGood) and TryStep(present, aGood) = Ok(_).
The MCK2 guarantee is relative to the domain-defined intent envelope (Explains). The domain chooses what “meaning-preserving” means; the kernel guarantees rejection only when the entire envelope fails.

​
Integration boundary (trusted)

  • Ordering and delivery of realtime updates
  • Database atomicity and transactions
  • Edge/server orchestration around verified transitions
  • Liveness beyond the modeled protocol

​
Effect State Machine

State space: EffectState = { network, mode, client, serverVersion }

​
Assumptions

  • The embedded client component itself satisfies the obligations of the client protocol kernel it instantiates.

​
Kernel theorems

  • (ESM1) StepPreservesInv — all effect-state transitions preserve the invariant.
  • (ESM2) Bounded retries (RetriesAreBounded) — retries never exceed MaxRetries.
  • (ESM3) FIFO processing — pending actions are processed in order; only the first can leave.
  • (ESM4) Pending preservation — pending' == pending or pending' == pending[1..].

​
System-level properties (proved)

PropertyMeaning
NoSilentDataLossEvery action in pending either stays in pending or is explicitly accepted/rejected
UserActionEntersPendingUser actions are guaranteed to enter the pending queue
FIFOProcessingActions are processed in submission order
OnlineIdlePendingMakesProgressSystem makes progress when online with pending actions

​
Integration boundary (trusted)

  • Mapping browser/network events to effect-machine events
  • Actual I/O execution of commands
  • End-to-end liveness assumptions

​
Multi-Project kernel

State space: multi-project model + per-project client state + effect orchestration

​
Domain obligations

Each concrete multi-project domain must prove: 
MultiInv(mm) ∧ MultiStep(mm, a) = Ok(mm′) ⇒ MultiInv(mm′)
where: 
MultiInv(mm) ≜ ∀pid ∈ dom(mm.projects). Inv(mm.projects[pid])

​
Kernel theorems

Assuming the obligation above:
  • (MPK1) All effect-state invariants proved for the single-project Effect State Machine lift to the multi-project setting.
  • (MPK2) Pending preservation across projects — pending actions are never silently lost; accept/reject removes exactly one action; conflicts preserve pending exactly.
  • (MPK3) Bounded retries and mode consistency.

​
Integration boundary (trusted)

  • Atomic application of verified multi-project transitions to storage
  • Realtime skew (partial arrival of multi-project updates)
  • Edge-function orchestration around verified transitions
  • Semantics of TouchedProjects beyond what is proved in the concrete domain

​
Domain- and application-level guarantees

Kernels are generic: they prove how invariants are preserved. Concrete domains determine what invariants mean by discharging the kernel obligations.
Domain / AppPrimary invariants proved by the domainKernels lifting these invariants
CounterNon-negativity (m ≥ 0)Replay, Authority
KanbanExact card partition (no duplication or loss); per-column WIP limitsReplay, Multi-Collaboration, Effect State Machine
CanonReferential integrity of nodes/edges/constraints; allocator freshnessReplay
ColorWheelMood bounds (S/L ranges); harmony coherence; graceful degradation to CustomReplay
ClearSplitConservation of money (sum of balances = 0); delta laws for expenses and settlementsReplay, Multi-Collaboration, Effect State Machine
Delegation AuthReferential integrity of grants/delegations; freshness of delegation IDsReplay
CollabTodoExact task partition; unique list names; membership constraints; referential integrity; soft-delete semanticsMulti-Project, Effect State Machine
In all cases, invariants are proved at the domain level and then preserved automatically by the kernels listed, assuming the corresponding domain obligations are discharged.

​
How to interpret these guarantees

This document draws a precise boundary around what is proved and what is not. What is claimed:
If a concrete domain discharges the stated obligations, then all kernel theorems apply to the Dafny-generated transition logic, independent of where that logic executes (CLI, browser, server, or edge function).
In particular:
  • Invariants proved at the domain level are preserved by kernel transitions.
  • Protocol and effect-machine properties hold for the verified state machines.
  • Rejection and retry guarantees are exactly those stated by the kernels.
What is not claimed:
  • That the entire application or deployment is verified end-to-end.
  • That networking, databases, realtime delivery, or authentication are correct.
  • That the specifications themselves are complete or free of modeling error.
Verified transition logic may run inside larger unverified systems. The guarantees apply to the logic itself, not to the surrounding infrastructure.
This separation is intentional: it keeps the verified core small, reusable, and auditable, while making the trust boundary explicit.

Domain obligations guide

Step-by-step walkthrough of writing and discharging domain obligations.

Type mappings reference

Complete Dafny-to-JavaScript type conversion reference with code examples.

Build docs developers (and LLMs) love

Get started for freeTalk to us