Canonical uses TLA+ to test whether a 16-year-old SQLite WAL bug hits dqlite

SQLite recently patched a database-corruption bug in how its Write-Ahead Log is checkpointed and reset. The defect had lived in the codebase since 2010 and is notable less for its real-world impact—which SQLite considers very low—than for how long it hid and how hard it was to reproduce. For Canonical’s dqlite team, which builds a distributed SQLite atop the same engine, the pressing question was whether their system inherits the flaw.

Rather than chase an elusive reproduction by hand, the engineers turned to TLA+, a formal specification language, to model SQLite’s WAL behavior and let a model checker surface the exact interleaving of steps that produces corruption. Their spec stays deliberately minimal: pages become unique incrementing integers, the WAL is a sequence and the database a set, and only the mechanics that matter—appending frames under the write lock and checkpointing under the checkpoint lock—are captured. The relevant shared-memory state reduces to three fields: walSalt (bumped on each WAL reset), mxFrame (the WAL length), and nBackfill (how many pages have been checkpointed).

With a faithful model of SQLite in hand, the plan is to build a second model describing how dqlite actually drives SQLite and then check whether the corrupting trace is reachable there. The write-up doubles as a practical argument for lightweight formal methods: modeling behavior abstractly can expose and explain rare concurrency bugs far faster than trying to trigger them in a running system, and can answer downstream ‘are we affected?’ questions with more confidence than testing alone.