16-year-old SQLite WAL checkpoint corruption bug found with TLA+

Category: Engineering post
Status: confirmed
Sources: Canonical dqlite write-up, HN discussion
Summary: Marco Manino and Alberto Carretero of Canonical's dqlite team published (2026-06-25) a TLA+ model of SQLite's write-ahead-log checkpointing that reproduced a data race present since 2010: when a checkpoint runs concurrently with a WAL reset, the checkpoint can fail to notice the reset and skip parts of transactions, corrupting the database. The model-checker surfaced the counterexample within 20 states. The authors report real-world impact as very low, note dqlite is not affected because it takes exclusive write locks during both append and checkpoint, and describe the SQLite fix as a single comparison of WAL salt values before and after checkpoint setup that skips the checkpoint when the salt changed.
Why it matters: SQLite is one of the most widely deployed databases, and a durable-storage race that hid for 16 years is a concrete case for formal modeling of concurrency invariants in storage engines.
Follow-up: Track the SQLite version that ships the salt-comparison fix and any downstream re-vendoring.