- Author
- Marco Manino and Alberto Carretero, dqlite team at Canonical
- Published
- 25 June 2026
- Kind
- Company engineering blog post with a worked model-checking example
- Original
- ubuntu.com/blog/hunting-a-16-year-old-sqlite-bug-with-tla-is-dqlite-affected
- Subject
- Checkable specs for coding agents
- Themes
- Checking the work, How things break
What it is
Marco Manino and Alberto Carretero are on the dqlite team at Canonical. The post explains a SQLite checkpoint bug. It then builds two TLA+ models, one for SQLite and one for dqlite.
What it says
- The post says the SQLite bug dates from 2010. It lasted 16 years with low real-world impact.
- The authors model two actions, appending and checkpointing. One invariant flags a missing page.
- The model-checker found a counterexample in only 20 states. It resembles SQLite's own report of the bug.
- A second model adds the write lock during checkpoints, as dqlite does. It finds no violation.
- The post says dqlite is not affected. Appending and checkpointing cannot run at the same time.
- SQLite fixed the bug with a single extra check. The same model-checking run then finds no error.
What evidence it gives
The evidence is a TLA+ model with a model-checker run. The run found a counterexample for SQLite and none for dqlite. The post shows C code excerpts and spec fragments. The full specification is linked in a gist.
Interests and limits
Canonical makes dqlite, so the team has an interest in the answer. The model is a simplified abstraction without readers. The conclusion covers one bug and two models. The long C code and TLA+ fragments were skimmed, not read line by line.
Connections
These links are this wiki's own reading, not claims the sources make.
- How we tracked down a 16-year-old SQLite bug. These describe one bug from two sides. Tailscale needed six months and 19 incidents to find it through telemetry. The model checker reached a counterexample in 20 states, once people knew what to model. Finding and confirming turn out to be different jobs.