A balanced ledger can still be wrong

The standard correctness check for a ledger is conservation: sum every balance, confirm that value was neither created nor destroyed. It’s a good check. It’s also much weaker than it feels — and building our verification around that discovery shaped how we test TulaDB.

Developer-preview note: this post describes the verification approach in TulaDB’s own Jepsen-style test harness. The harness, its workloads, and their honest coverage limits are documented in how we verify correctness.

Six faults conservation cannot see

Conservation is an equation over totals, and equations over totals are satisfied by many wrong ledgers. Each of the following leaves the books perfectly balanced:

• A lost acknowledged write — if the sum still balances without it.
• A phantom write — committed, though no client ever invoked it.
• A resurrected rejection — refused, yet somehow committed later.
• A double-apply — one transfer identity applied at two positions, if it happens to net out.
• Misattribution — the right total moved between the wrong accounts.
• Balances that disagree with the recorded history — as long as they disagree consistently.

A database that moves value between the wrong accounts, or loses an acked write while inventing an unacked one, passes the conservation check with a green tick.

The overdraft that balances exactly

The sharpest version of the problem: conservation cannot see an overdraft. An account opens with 100. Two concurrent transfers of 60 arrive; each is individually affordable, together they are not. If a lost serialization lets both commit:

account 0 = -20        ← driven through a floor of 0
total     = unchanged  ✓ the books balance exactly

Double-entry is intact — value was neither created nor destroyed. It was merely spent by someone who did not have it. No sum, on any snapshot, at any point in time, will ever flag this.

The fix: replay the ledger’s own order

The only check that catches all of the above is a model replay: reconstruct the committed history and demand that the database equal a replay of it.

Two properties of TulaDB make this cheap rather than heroic. First, every committed record carries its position in the total order — (batch_seq, batch_index) — plus its transfer identity, so the checker verifies against the ledger’s own order instead of trying to infer one from concurrent client timelines. Second, rejected outcomes are durable records, so “refused” is a checkable state, not an absence.

The replay then re-decides everything at its own position: every acknowledged write must be present, every rejection must stay rejected, every balance must be attributable to the recorded history — and every admission decision must have been legal at its position. That last clause is what catches the balanced overdraft: re-deciding each transfer of 60 against the state where it actually landed exposes the second one as inadmissible, however clean the totals look.

The same replay runs over the two-phase lifecycle, where it catches the transitions client-side checks can miss entirely: a commit that lands after a rollback, a double-commit, a leaked hold whose acknowledgement never reached anyone.

Verdicts from what was recorded, not what was told

Client-side checkers derive verdicts from what clients were told. The model derives them from what the ledger recorded — so it can see a violation whose acknowledgement was lost in a partition. And the harness distrusts vacuous success: a limits run in which nothing was ever refused reports “limits not exercised” rather than letting an empty green stand. A refusal, in that workload, is the correct answer.

None of this makes conservation useless — it runs on every workload, continuously. It makes conservation the floor. The interesting bugs live in the gap between “the books balance” and “the books are right,” and that gap is precisely where a financial-state engine has to be tested.

In the docs: How we verify correctness covers the full workload matrix, the fault menu, and — just as deliberately — what the current campaigns don’t yet claim.