Proven, not sampled
Example tests prove the engine handles the cases we thought of. For the component that decides whether money leaves your account, that is the weaker claim.
423 tests · 600,000 generated decisions · 17 of 17 mutants caught
Properties, not examples
A property holds for every input, not for the ones we thought of.
Each of the twenty-one invariants is stated as a property that must hold for all inputs, and a generator searches for a counterexample. When it finds one it shrinks it to the smallest failing case — the difference between “something broke” and “here is the one-line reproduction.”
The interesting failure is never the case you imagined. It is an amount one micro-unit over a cap, a counterparty that is the empty string, a permission expiring on the same millisecond as the payment. Roughly 11,700 assertions run per suite.
Conservation — that authorized spend never exceeds the window cap — is checked against an independent tally, not by asking the budget whether it agrees with itself. An invariant that consults the component under test proves nothing.
Deterministic simulation
600,000 decisions across 372 simulated years, replayable from a seed.
The discipline FoundationDB pioneered and TigerBeetle built a financial database on: control every source of non-determinism — clock, randomness, faults — so a run is a pure function of its seed. Then generate hostile histories by the thousand, assert the invariants after every step, and replay any failure exactly instead of chasing it.
Property tests ask whether a single decision holds. This asks the harder question: does the system hold across a long hostile history — permissions granted and revoked and expiring, clocks jumping days, budgets filling and ageing out, an agent proposing attacker payments throughout? Payment bugs live in histories, not in single calls.
This was cheap because the system was built to be simulatable: the clock is injected everywhere, the engine is pure, the price resolver is a parameter, and nothing in the decision path reads a hidden global. That was a constraint from the first commit, not a retrofit.
Three defects this found in itself
The interesting output of a test suite is what it caught, not that it passed.
The payload was never hashed
Canonical serialization used a top-level key list as a filter, which JSON applies at every nesting level — so the payload hashed as empty and editing a past amount was undetectable. Tamper-evidence that does not cover the payload is decoration. Caught by a tamper test, fixed, and the fix is pinned.
A sweep that looked exhaustive and wasn’t
Seeding the generator directly left adjacent seeds correlated — seeds 1, 2 and 3 opened within 0.002 of each other. A sweep over seeds 1..N would have explored a sliver of the space while appearing thorough. That is the worst class of testing bug, because it inflates confidence rather than failing. The state is avalanched now, with a test pinning decorrelation.
Spend that doubled where nobody could see it
Two passes overlapping recorded 6 USDC of spend for 3 USDC of payouts. The append-only log refused the duplicate events correctly; the in-memory ledger recorded them anyway, because the append's return value was discarded. What makes this the worst of the three is that it was invisible — replaying the log afterwards gives the right total, so every audit path, every export and every restart showed no problem. The corruption lived only in the instance actually deciding, where a campaign would start refusing payouts as pool-exhausted while half its recorded spend never happened. Found by injecting faults into the real runtime rather than by reading the code.
All three are listed because a testing page that only reports passes is a marketing page. The reason to trust the numbers above is that the same process caught these.
Honest limits
What is not covered, named — because a gap you can name is one somebody can hold you to.
TigerBeetle runs two millennia of simulated time per day on a thousand cores. This runs 372 years in 3.6 seconds on one. Same method, not the same coverage, and it would be dishonest to imply otherwise.
Not yet covered: concurrency against a durable store, which does not exist yet; fault injection between reserving and committing; chain verification under concurrent append. Named rather than glossed — because a gap you can name is one somebody can hold you to.