How we verify correctness

A ledger’s guarantees are only as good as the adversarial testing behind them. This page describes how TulaDB is verified — and, just as deliberately, what that verification does and doesn’t cover yet. Evidence bundles behind the summaries here are part of the developer-preview evaluation package.

Invariants, checked twice

The core invariants — debits equal credits under every consistent view, no half-applied transfer, no double-application, holds always in a legal lifecycle state — are enforced on the write path and re-checkable after the fact: an offline verifier (tuladb_verify_store, shipped in the release binaries) opens a stopped store through recovery and re-runs the consistency checks, and tiered ledgers can produce a per-tier reconciliation whose discrepancy must be zero. An AddressSanitizer and UndefinedBehaviorSanitizer build runs the engine’s full test suite on Linux (macOS runs a portability build and the core test slice), alongside bounded proof and fuzz gates over the WAL, storage, and recovery paths, and fault-injection tests for crash, partition, disk-full, and fsync-failure scenarios.

Deterministic simulation

Two simulators run the engine under a controlled scheduler and fault plan, so a failure reproduces from its seed: an in-process deterministic-simulation family (crash, partition, per-node clock-rate skew, client retry across failover) and a swarm simulator that drives a whole cluster. Both compare more than balances — they digest each idempotency identity’s phase and position across nodes, and the swarm simulator’s late-retry oracle is strict: any re-post of an acknowledged transfer fails the run.

Replicas compared at one log position

tulactl digest-at-cut --seq S asks a node for order-independent digests of every replicated component — balances, open holds, in-flight stages, the idempotency index (including identities evicted to disk), history above the purge floor, registries, features, cluster config, retention coverage, and the WAL chain head — captured at exactly log position S. Asking every node for the same S turns “the replicas agree” from an inference into a check, and it’s how fault-injection campaigns end: stop the load, pick a cut, compare. Nodes that evicted different identities to disk still produce the same idempotency digest.

Jepsen-style fault injection

TulaDB is internally tested with Jepsen-style fault injection: a purpose-built harness run against 5-node clusters (Docker containers) while faults are injected. Its most recent recorded campaign, on 2026-08-15 against a development build, ran 17 configurations — 14 workloads plus two-phase variants of three of them — under partition, packet, kill and pause faults. This is our own testing, not an external audit or certification.

What the workloads check:

Property	Workload examples
Money conservation — total posted balance invariant under faults	bank
Linearizability	counter, follower-read session guarantees
Exactly-once under replay — same txn_id resubmitted, even with different amounts	idempotence, indefinite
Two-phase lifecycle — no leaked holds, terminal-transition races settle uniquely	twopc
Cross-tier atomicity — position and settlement mirrors stay equal	tiered, tiered-batch
Transaction-order soundness — cycle detection over list-append histories (Elle)	elle
Admissibility — no overdraft admitted, ever, under concurrency	limits
Read-path equivalence — filtered equals derived; paged equals one-shot	query

The harness’s fault menu includes network partitions (including leader isolation and ring majorities), process kills up to and including the whole cluster, process pauses, packet loss/corruption/reordering, dynamic membership changes during load — and a set of storage faults built specifically for TulaDB’s on-disk layout: bit-flipping and truncating WAL segments, snapshots, and Raft metadata; wiping a replica and rebuilding it from peers; and restoring a node from a stale-but-internally-valid snapshot, precisely the case a checksum cannot catch. The August campaign used only the partition, packet, kill and pause faults; the membership and storage faults had not yet been run in a campaign.

Why conservation alone isn’t the test

A balance-sum check can pass while the ledger is wrong: a lost acknowledged write and a resurrected failed write can cancel; two concurrent, individually-affordable debits can overdraw an account while the books still balance. The harness therefore doesn’t just check totals — it replays the ledger’s own committed order (batch_seq, batch_index) against a model and requires every acknowledged write to be present, every rejection to stay rejected, every balance to be attributable, and every admission decision to have been legal at its own position in the order.

Results, stated carefully

In the 2026-08-15 campaign — 17 configurations under partition, packet, kill and pause faults — no checker returned invalid: 12 configurations were valid and 5 returned unknown, so no lost acknowledged write, double-application, conservation violation or admitted overdraft was found. Unknown means not falsified and not certified either — here a paged history read under fault that the checker could not attribute, or a tiered hold on a downed node that the drain could not reach — and the harness treats it as unfinished work rather than success.

Fault-injection has found real bugs — that’s the point. One example: a history query silently omitted committed rows under a specific eviction race. It was fixed with deterministic regression tests — and a code audit of the class of defect found two sibling instances the harness structurally couldn’t reach. One in three was harness-visible; the other two fell to review. Both methods stay in the loop.

Scope: what this doesn’t claim yet

The campaign results above were produced on development builds before 0.0.1-preview, not on the release itself; the release’s own chaos gate has since passed on the release build (verdict), and its six-hour multi-region soak has not run yet. Treat them as evidence about the design and the test method, and re-run against the build you evaluate.

Honesty about coverage is part of the method. As of that campaign: clock-skew faults haven’t run on real VMs (containers share the host clock); the storage-fault and membership nemeses had not been run; runs are 150 seconds long, so long-running resource behaviour is left to separate soak testing, not this harness; and reservation-expiry has a written workload not yet run against clusters. Verdicts under randomized fault timing vary run to run — the claim is about the composition of evidence, not any single green cell.

Chaos and scale campaigns

Beyond the fault-injection harness’s small-cluster precision, longer campaigns run the full platform on EC2 across three availability zones under sustained load with fault injection, checking exact conservation at scale — roughly 15 to 33 million units moved per one-hour run in the August campaign, summing correctly to the unit — and producing the sizing guidance in Limits and the published evidence in Resilience.