Hunting a 16-Year-Old SQLite Bug with TLA+: Is dqlite Affected?
Canonical's dqlite team used TLA+ to model a 16-year-old data race in SQLite's WAL checkpoint code — finding a corruption path in 20 model states, proving dqlite immune because its stop-the-world checkpoint prevents the race, and confirming SQLite's one-line salt-check fix is sufficient.
A bug present in production code for 16 years is not a failure of testing. Tests find bugs your mental model predicts. Formal methods find bugs your mental model missed entirely — because they enumerate every interleaving of concurrent actions you did not think to check.
Source
Hunting a 16-year-old SQLite bug with TLA+: is dqlite affected?
By: Marco Manino and Alberto Carretero, dqlite team at Canonical
Published: Jun 25 2026
Type: Engineering article
Canonical’s dqlite team used TLA+ to reconstruct a subtle SQLite data race and prove their own system unaffected — a clean example of formal methods applied to a real production bug rather than an academic exercise.
How TLA+ Exposed a SQLite Data Race That Survived 16 Years
SQLite operates in WAL mode by writing new pages to a Write Ahead Log file rather than directly updating the database. Eventually those pages are checkpointed — copied from the WAL back into the main database file. Once all pages are checkpointed, the WAL can be reset: the salt counter increments, mxFrame resets to zero, and the next writer begins overwriting from the start of the file. This mechanism lets readers and writers proceed concurrently without blocking each other.
The bug, present since 2010 and publicly disclosed in March 2026, is a data race between a checkpoint operation and a concurrent write. It requires exactly the right sequence of six overlapping operations across two connections — which is why it survived 16 years with very low real-world impact but genuine corruption potential.
The Canonical team built a TLA+ model with five shared variables: wal (the WAL contents as a sequence), db (the database as a set), nBackfill (pages already checkpointed), mxFrame (current WAL length), and walSalt (reset counter). Actions map directly to SQLite’s C code: WalAppendTakeLock, WalAppend, CheckPointCopyHeader, StartCheckpoint, and Checkpoint. The key modeling decision is that pWal->hdr is a local copy of the WAL index header taken at a fixed point in time, while pInfo is a volatile pointer to shared memory that can change between reads — so the two must be modeled as separate variables that can diverge mid-operation.
Running the model checker with the invariant NoPageIsLost — every frame added to the WAL must eventually appear in the database — produces a counterexample in 20 states. The sequence matches SQLite’s own bug report almost exactly:
A first checkpoint completes fully, moving all pages to the database and leaving the WAL eligible for reset. A second checkpoint starts immediately and copies the WAL index header, recording safeMxFrame = 2 and pWalSalt = 0. Before the second checkpoint acquires its read lock, a writer resets the WAL: walSalt increments to 1, mxFrame resets to 1, nBackfill resets to 0, and the writer appends a new page at position 1. The second checkpoint now holds a stale safeMxFrame = 2 against a WAL that only has one frame. It proceeds, sets nBackfill = 2, and finishes — the stale value now tells any future checkpoint that frames 1 and 2 of the current WAL generation have already been backfilled. They have not. When a third checkpoint runs, it skips those frames entirely. The page written right after the WAL reset is silently lost, and the database file goes corrupt.
The fix SQLite shipped adds a single memcmp after acquiring the read lock: compare the live WAL salt against the salt recorded in the local copy at the start of the checkpoint. If they differ, the WAL was reset while the checkpoint was setting up — skip the backfill and return without modifying nBackfill. In TLA+, this becomes a conditional inside the Checkpoint action: if walSalt ≠ pWalSalt, leave db and nBackfill unchanged and reset the checkpoint state. The model checker finds no invariant violation with this change in place, confirming the fix is both necessary and sufficient.
dqlite is immune because it uses a stop-the-world checkpoint: before calling sqlite3_wal_checkpoint_v2, it acquires all SHM locks including the write lock, preventing any concurrent writer from resetting the WAL while the checkpoint is in flight. The TLA+ model for dqlite is an extension of the SQLite spec — it imports the base spec with INSTANCE and overrides the CheckPointCopyHeader action to require writeLock = "takenForCheckpoint". Under this constraint, the model checker finds no counterexample, because the write lock acquisition order makes the race impossible.
The article is a good demonstration of TLA+’s practical workflow for storage system bugs: write a minimal spec with only the variables and actions involved in the race, define an invariant, run the model checker, read the counterexample trace, understand the bug, apply the fix to the spec, re-run. The spec ends up smaller than the C code it models because it discards all the I/O, error handling, and pagination logic that does not participate in the concurrent interleaving.
My take
The 20-state counterexample is the number to carry. A concurrent bug that survived 16 years in one of the most tested codebases in open source took the TLA+ model checker 20 states to find. This is not a statement about SQLite’s test quality — it is a statement about what tests verify. Tests confirm specific sequences run by a human or a fuzzer. Model checkers enumerate all sequences under a given abstraction, including interleavings nobody thought to generate.
Where this is useful
- Storage systems, databases, or any code where multiple concurrent agents share state through a combination of locks and volatile shared memory
- When you want to verify that a proposed fix is sufficient rather than just plausible — the same model that found the bug can confirm the patch
- When NOT applicable: single-threaded code, or concurrent code with no shared mutable state — the model checker generates the most signal where state space is defined by lock acquisition order and shared variable reads
Apply this: When a concurrent bug seems too rare to reproduce, write a TLA+ spec with the smallest state that captures the race — the model checker will enumerate the path your tests never generated.
What I want to remember
Remember: TLA+ does not find bugs by running code faster — it finds bugs by abstracting away everything except the shared state and the ordering of operations that modify it.