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.

ClearSplit tracks shared expenses and settlements among a group of people. Its central guarantee—the Conservation Theorem—states that the sum of all balances is always exactly zero: money cannot appear or disappear. This is not an assertion or a test; it is a mathematical theorem proved in Dafny and preserved by construction across every operation.

​
Domain model

The model holds three entity types. Money values are integers (representing cents) to avoid floating-point errors. 
type Money = int  // cents

datatype Expense = Expense(
  paidBy: PersonId,
  amount: Money,
  shares: map<PersonId, Money>,  // each participant's consumed share
  shareKeys: seq<PersonId>       // ordered keys for compiled iteration
)

datatype Settlement = Settlement(
  from: PersonId,
  to: PersonId,
  amount: Money
)

datatype Model = Model(
  members: set<PersonId>,
  memberList: seq<PersonId>,  // ordered, matches members
  expenses: seq<Expense>,
  settlements: seq<Settlement>
)

datatype Action =
  | AddExpense(e: Expense)
  | AddSettlement(s: Settlement)

​
Module structure

The code is split into two Dafny modules to separate the user-facing contract from its proof: ClearSplitSpec (abstract module) — defines all types, predicates, function signatures, and the key lemma signatures as abstract declarations. This is the surface you review when you want to understand the guarantees without reading proofs. ClearSplit (refinement module) — provides all implementations and proofs. The abstract lemma signatures are discharged here with full proof terms. 
// In ClearSplitSpec (abstract — just the signature):
lemma Conservation(model: Model)
  requires Inv(model)
  ensures SumValues(Balances(model)) == 0

// In ClearSplit (implementation — full proof):
lemma Conservation(model: Model) {
  BalancesEquiv(model);
  ZeroBalancesSum(model.members);
  ApplyExpensesPreservesSum(...);
  ApplySettlementsPreservesSum(...);
}

​
Key theorems

​
Conservation Theorem

The sum of all member balances is always zero. No money is created or destroyed by any sequence of expenses and settlements. 
Inv(model) ⟹ SumValues(Balances(model)) = 0

​
AddExpense Delta Law

When an expense e is added:
  • If the payer is not a share owner: balance(payer)' = balance(payer) + amount
  • For each share owner (not the payer): balance(p)' = balance(p) - shares[p]
  • If the payer is also a share owner: balance(payer)' = balance(payer) + amount - shares[payer]
  • All other balances are unchanged.

​
AddSettlement Delta Law

When a settlement s is recorded:
  • balance(s.from)' = balance(s.from) + amount (payer owes less)
  • balance(s.to)' = balance(s.to) - amount (recipient is owed less)
  • All other balances are unchanged.

​
ExplainSumsToBalance

A person’s current balance equals the sum of all their individual transaction deltas across every expense and settlement. This provides an auditable history: you can reconstruct the exact balance from the sequence of transactions. 
∀p ∈ members. SumSeq(ExplainExpenses(model, p)) = GetBalance(model, p)

​
Kernel variants

ClearSplit is proved against three kernels, covering local use, collaborative use, and cloud deployment:
DirectoryKernelFeatures
clear-split/ReplayUndo/redo, local state
(via ClearSplitMultiCollaboration.dfy)Multi-CollaborationOffline clients, concurrent edits
clear-split-cloud/Effect State MachineBackend persistence (Supabase or Cloudflare)

​
Running the app

cd clear-split
npm install
npm run dev
For the cloud variant with backend persistence: 
cd clear-split-cloud
npm install
npm run dev

Replay kernel

Local undo/redo with invariant preservation across all history operations.

Multi-Collaboration kernel

Server-authoritative state with offline client support and minimal rejection.

Effect State Machine

Bounded retries and pending-action preservation for the cloud variant.

Guarantees reference

Precise statement of what is proved, what is assumed, and what is trusted.

Build docs developers (and LLMs) love

Get started for freeTalk to us