Share on: Facebook Twitter LinkedIn This article was written by Marco Manino and Alberto Carretero, dqlite team at Canonical . 1. Anatomy of a SQLite bug Recently SQLite published a new version with a fix to a long-standing bug in the way that the Write Ahead Log (WAL) is checkpointed that leads to the corruption of the database. The important aspect of this bug is not its real-world impact (which is very low) but how long it has been in the repository, how difficult it was to find it, and how difficult it was to reproduce it. Indeed the bug has been present since 2010, for 16 years ! Also, the crucial question for us, the dqlite team, is: can dqlite be affected by this? In order to find out, we first need to be able to understand the exact sequence of steps that leads to database corruption. To do that, we will be using TLA + to model SQLite’s behavior and quickly find a trace that allows us to reason about the bug.…