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.

The Multi-Collaboration kernel addresses a core challenge in server-authoritative collaborative apps: clients submit actions based on stale server versions. A client editing offline may reference anchors that no longer exist, positions that have shifted, or columns that were renamed. The kernel rebases each incoming action through the intervening history, then tries a small ordered candidate set before accepting or rejecting — and proves that rejection happens only when no meaning-preserving interpretation could succeed.

​
The problem: stale clients

When multiple clients edit concurrently, a client’s action may arrive with a base version that is behind the server. Naïve rejection is safe but harsh — often the user’s intent can be preserved even when the exact action no longer applies. Naïve acceptance without rebasing is unsafe — it can violate global invariants. The Multi-Collaboration kernel takes a third path: intent-relative reconciliation with a proved reject boundary. 
Client (stale)
   |
   |  (orig action, baseVersion)
   v
+------------------------------+
|        Server Dispatch       |
+------------------------------+
            |
            | rebase against intervening history
            v
     rebased intent
            |
            | enumerate finite candidates
            v
+------------------------------+
|   Candidates (ordered)       |
|                              |
|  1. rebased intent           |
|  2. universal fallback       |  ← intent envelope (proved)
|  3. heuristic candidates     |  ← outside proof, improves UX
+------------------------------+
            |
            | try in order with TryStep
            v
     +------------------+
     |  first success?  |
     +------------------+
        |           |
       yes         no
        |           |
        v           v
+---------------+  Reject
|  Accept       |
|  - append log |
|  - update     |
|  - invariant  |
+---------------+

​
ServerState

datatype ServerState = ServerState(
  present: D.Model,
  appliedLog: seq<D.Action>,
  auditLog: seq<RequestRecord>
)

function Version(s: ServerState): nat { |s.appliedLog| }
The server maintains the current model, a log of every accepted action (used for rebasing), and an audit log of every request record including the original action, rebased action, chosen candidate, and outcome.

​
Anchor-based placement

Instead of fragile positional indices, the domain models placement intent using anchors: 
Place = AtEnd | Before(anchor) | After(anchor)
A move action carries Place rather than a raw index. When an anchor card is missing (deleted or moved by another client), the server can fall back to AtEnd or another heuristic without losing the user’s core intent (move to this column).

​
Domain obligations

The Multi-Collaboration kernel requires domains to prove three groups of obligations: 
lemma InitSatisfiesInv()
  ensures Inv(Init())

lemma StepPreservesInv(m: Model, a: Action, m2: Model)
  requires Inv(m)
  requires TryStep(m, a) == Ok(m2)
  ensures  Inv(m2)
The domain must provide four elements that define how intent is preserved under concurrency:Rebase(remote, local) — a total function that transforms a local action assuming a remote action happened first. Folded over a suffix to rebase through multiple intervening actions:
function RebaseThroughSuffix(suffix: seq<Action>, a: Action): Action
  decreases |suffix|
{
  if |suffix| == 0 then a
  else
    RebaseThroughSuffix(suffix[..|suffix|-1],
                        Rebase(suffix[|suffix|-1], a))
}
Candidates(m, a) — a finite ordered list of concrete actions the server will try in order:
function Candidates(m: Model, a: Action): seq<Action>
Explains(orig, cand) — a ghost predicate defining which candidates count as meaning-preserving interpretations of the original request (the “intent envelope”):
ghost predicate Explains(orig: Action, cand: Action)
CandidatesComplete — the completeness lemma that ties the envelope to the candidate set: if an admissible interpretation exists and would succeed, it must appear in Candidates:
lemma CandidatesComplete(m: Model, orig: Action, aGood: Action, m2: Model)
  requires Inv(m)
  requires Explains(orig, aGood)
  requires TryStep(m, aGood) == Ok(m2)
  ensures  aGood in Candidates(m, orig)

​
Dispatch

The server’s dispatch function ties everything together: 
function Dispatch(s: ServerState, baseVersion: nat, orig: D.Action): (ServerState, Reply)
  requires baseVersion <= Version(s)
  requires D.Inv(s.present)
  ensures  D.Inv(Dispatch(s, baseVersion, orig).0.present)
{
  var suffix := s.appliedLog[baseVersion..];
  var rebased := D.RebaseThroughSuffix(suffix, orig);

  var cs := D.Candidates(s.present, rebased);

  match ChooseCandidate(s.present, cs)
    case Ok(pair) =>
      // Accept: append chosen to log, update present
      ...
    case Err(_) =>
      // Reject: no candidate succeeded
      ...
}
ChooseCandidate tries candidates in order and returns the first success: 
function ChooseCandidate(m: D.Model, cs: seq<D.Action>): D.Result<(D.Model, D.Action), D.Err>
  decreases |cs|
  ensures ChooseCandidate(m, cs).Ok? ==>
          D.TryStep(m, ChooseCandidate(m, cs).value.1) == D.Ok(ChooseCandidate(m, cs).value.0)

​
Kernel theorems

lemma DispatchPreservesInv(s: ServerState, baseVersion: nat, orig: D.Action)
  requires baseVersion <= Version(s)
  requires D.Inv(s.present)
  ensures  D.Inv(Dispatch(s, baseVersion, orig).0.present)
The kernel only transitions via a successful TryStep, and MC2 guarantees that TryStep success preserves Inv. This is the primary safety theorem.
lemma DispatchRejectIsMinimal(
  s: ServerState, baseVersion: nat, orig: D.Action,
  aGood: D.Action, m2: D.Model)
  requires baseVersion <= Version(s)
  requires D.Inv(s.present)
  requires D.Explains(D.RebaseThroughSuffix(s.appliedLog[baseVersion..], orig), aGood)
  requires D.TryStep(s.present, aGood) == D.Ok(m2)
  ensures  !Dispatch(s, baseVersion, orig).1.Rejected?
Stated plainly: if any meaning-preserving interpretation of the rebased request would succeed, the server will not reject. The proof proceeds by applying CandidatesComplete to show that aGood must appear in the candidate list, then ChooseCandidateFindsGood to show that the candidate search will find it.This is a guarantee relative to the domain-defined intent envelope (Explains). The domain chooses what “intent preserved” means; the kernel guarantees that rejection happens only when the envelope is impossible to satisfy.

​
Client-side state

The kernel also provides verified client-side operations for optimistic updates: 
datatype ClientState = ClientState(
  baseVersion: nat,           // last synced server version
  present: D.Model,           // current local model (optimistic)
  pending: seq<D.Action>      // actions waiting to be flushed
)
Key client functions:
FunctionEffect on pending
ClientLocalDispatch(client, action)Appends action to pending
ClientAcceptReply(client, newVersion, newPresent)Removes pending[0], re-applies rest
ClientRejectReply(client, freshVersion, freshModel)Removes pending[0], re-applies rest
HandleRealtimeUpdate(client, serverVersion, serverModel)Preserves pending exactly
ReapplyPending re-applies pending actions on top of a new server model to maintain the optimistic view after a realtime update: 
function ReapplyPending(model: D.Model, pending: seq<D.Action>): D.Model
  decreases |pending|
{
  if |pending| == 0 then model
  else
    var result := D.TryStep(model, pending[0]);
    var newModel := match result
      case Ok(m) => m
      case Err(_) => model;
    ReapplyPending(newModel, pending[1..])
}

​
Concrete example: Kanban moves

In the Kanban domain, a MoveCard action carries anchor-based placement. The server tries three candidates for each move:
  1. The rebased placement (original intent after rebasing)
  2. AtEnd — universal fallback (in the intent envelope)
  3. Before(first) — heuristic (outside the proof)
The kernel proves that Before(first) is redundant: if it succeeds, AtEnd also succeeds (BeforeFirstImpliesAtEnd). This justifies defining Explains to cover only the rebased placement and AtEnd, giving a clean guarantee:
A move is rejected only if neither its intended placement nor the universal fallback AtEnd could be applied without violating invariants.

​
Integration boundary (trusted)

  • Ordering and delivery of realtime updates
  • Database atomicity and transactions
  • Edge/server orchestration around verified transitions
  • Liveness beyond the modeled protocol
The candidate set may include heuristics beyond the intent envelope. These improve UX (e.g., layout stability) without enlarging the proof surface. The proof establishes a lower bound on acceptance; the implementation is free to be more permissive.

Effect State Machine

Client-side orchestration layer built on top of Multi-Collaboration.

Multi-Project kernel

Extends Multi-Collaboration to cross-project operations.

CollabTodo app

Full example using Multi-Collaboration with Supabase or Cloudflare.

Guarantees reference

Precise trust boundaries for the Multi-Collaboration kernel.

Build docs developers (and LLMs) love

Get started for freeTalk to us