Testing samples time: SQLite's WAL reset bug and the case for proofs

SQLite is tested to a standard most software never approaches. Its test suite is hundreds of times the size of the library itself, it reaches the 100% modified condition/decision coverage that avionics software is held to, and it runs under continuous fuzzing. If thorough testing were ever enough on its own, SQLite is where it would be.

And yet a data race lived in its write-ahead log for sixteen years. It corrupted a production database at Tailscale nineteen times over six months before anyone understood why. It was so rare that the SQLite developers, once they had found it, had to add code to their own test harness just to provoke it.

Proofs have a reputation as the slow option, the heavyweight tool you reach for in avionics or cryptography when you have time to spare. This is a case for the opposite view, argued on the least sympathetic example we could find. We checked one property, taken straight from SQLite's own WAL specification, by reasoning rather than by running the code, and that was enough to locate the exact window this bug lives in, without the race ever having to happen.

The bug, briefly#

SQLite records recent writes in a write-ahead log and later folds them into the main database file, a step called a checkpoint; once a log is fully checkpointed, a writer may reset it and start again at the beginning. The bug is a rare data race between a checkpoint and a concurrent reset: the checkpoint misses the reset, keeps working from a stale view of the log, and writes stale log data back over the database file. Committed writes disappear, and the file can fail PRAGMA integrity_check. SQLite documents the bug in its own WAL spec; Tailscale, who hit it repeatedly in production, spent months tracing it with the SQLite developers and wrote that story up; Carl Sverre, writing at Antithesis, reproduced it by searching schedules. SQLite fixed it in version 3.51.3. Ours is a fourth account, by a different method.

Why testing can miss a bug like this#

The bug survived sixteen years of excellent testing for one reason: it is rare in time, and testing samples time. To see it, the exact interleaving has to occur: one connection resets the log in the same narrow instant another is midway through a checkpoint. You can run that workload for months and never land on it.

It is not rare in place, though. The interleaving corresponds to a fixed, small region of the code, and that is the opening: enumerate the schedules a piece of code admits, instead of sampling them by running it, and you never need the rare moment to arrive.

The property, taken from the spec#

One sentence in, a runnable bug out. The developer writes the intent; the Aretta backend does the rest, automatically:

Aristo, the verification tool we build, starts from an intent: a property stated in plain language, the way you would put it in a design doc. The durability bug we found in Turso started from an intent too. Here, the intent is a standard durability claim, and it is the claim SQLite's own WAL documentation already makes:

After a checkpoint, the database file reflects every committed frame up to the checkpoint point. A checkpoint never makes committed data invisible.

That sentence, an Aristo intent lifted straight from the WAL spec, is the whole input. Everything after it runs on Aretta's verification service. The service maps the intent to a formal statement and to a formal model of the checkpoint and reset protocol, then checks that model against the property, and that check is what surfaced the bug. Stated over the value a reader returns for a page, the property becomes the model's durability invariant:

-- durability: an actor with an open read transaction reads, for every page,
-- exactly the committed value as of when its transaction began. A lost
-- committed write, or a value resurrected from an overwritten log frame,
-- makes this false.
def durInv (c : Config) : Bool :=
  c.th.all (fun t => readerDurable c.shm t.loc) && freshDurable c

The check asks one question: does every interleaving of the checkpoint and reset protocol preserve durInv? The objection to preempt here is that we knew the answer and steered toward it, so it is worth being exact: the input was that one sentence. We did not write the formal statement, the model, or the interleavings, and nothing we gave the service named a bug, a place to look, a symptom, or a fix. We read the fix only afterward, to confirm the window matched. We brought exactly one piece of prior knowledge: we pointed the service at the WAL and checkpoint code rather than at all of SQLite, and durability is where any verification of a write-ahead log begins. Neither choice says anything about this defect. Everything else came from the infrastructure.

The answer is no, and the failing case is concrete: a fifty-three-step interleaving of a writer, a passive checkpointer, and a reader ends in a state where durInv is false. That is a theorem, checked by the Lean kernel:

theorem ce1_violates_durability :
    (run initReset schedCE1).map durInv = some false := by decide

The counterexample is small enough to print. A schedule in the model is nothing but a list of actor ids, one per sub-operation, and schedCE1 is fifty-three of them. Laid out on a timeline, the race is visible to the eye: the checkpointer caches its view of the log just before the reset lands, and everything that follows executes faithfully against that stale snapshot.

The counterexample also violates an invariant SQLite's own source comments assert, that "the nBackfill number is never greater than WalIndexHdr.mxFrame" (src/wal.c:342), evidence that the model tracks the real protocol rather than a caricature of it. And the fix guards exactly this window: version 3.51.3 adds a check that, after the checkpoint takes its read lock, detects that the log was reset out from under it and declines to write the stale data back.

From the formal model to the binary#

A counterexample in a formal model is a mathematical refutation: the Lean kernel certifies that the modeled protocol can reach a state where durInv is false. What it refutes, though, is the model, and a model can misdescribe the code it stands for. Aretta's backend discharges that doubt automatically: it replays the counterexample's schedule against the real library, holding a checkpoint inside the window while a writer resets the log. What reaches the developer is a runnable reproduction on a stock build, not a claim about a model. Under that schedule, a stock build of 3.51.2 loses committed rows, and in most runs the file is corrupted as well. A stock build of 3.51.3, under the identical schedule, does neither.

The stall the schedule needs is not exotic. A pause of a few milliseconds at the right point, the kind an ordinary scheduler hands out for a page fault or a slow syscall, is enough. That is how the bug reached production.

Search and reasoning#

Antithesis reproduced this bug by searching schedules; we located it by reasoning about them. The two routes are complementary. Search needs no formal model and is the right tool when you cannot build one: it explores executions until one trips an assertion. Reasoning needs a model, and in exchange it hands you the mechanism itself: the violated property, a machine-checked counterexample, and the exact window in the code, all before the code runs once. To be clear about credit, we did not find this bug; SQLite and Tailscale did. We showed that one property, taken from the spec, is enough to pin it down.

The mindset this should change#

The slow path to this bug was real: months of production corruption, forensic telemetry in a live system, and in the end, test-harness code written just to force the bug. The reasoning path was a property and a formal model, and it skipped all of that: the incident, the irreproducible flake, the triage.

Formal methods have long been filed under caution, a luxury for teams with time and budget to spare. What made verification elusive was its cost, and that cost is falling. As it falls, the arithmetic turns over: reasoning about where a bug must be is cheaper than waiting for it, reproducing it, and triaging it after an outage. The deterministic test the reasoning leaves behind is a standing guard that re-runs on every change. On software tested as thoroughly as any on Earth, a failure that took months to run down in production fell out of a single sentence of its own spec. Testing samples time. A proof does not have to.

A closing indulgence: the property above is not new. It is the WAL specification, which SQLite has published all along. So, at the risk of hindsight bravado, the bug was checkable the day it was written in 2010, and finding it never needed the race to happen even once. Aristo did not exist in 2010. Alas.