Hunting a 16-year-old SQLite WAL bug with TLA+: is dqlite affected?

By Marco Manino and Alberto Carretero (dqlite team at Canonical) Published on 25 June 2026

The Anatomy of a SQLite Bug

SQLite recently released a patch for a bug that had been lurking in its codebase for 16 years. The issue resides in the Write Ahead Log (WAL) checkpointing mechanism, which, under specific conditions, can lead to total database corruption.

While the actual real-world frequency of this bug is high very low, its significance lies in three areas:

1. Its longevity in the repository.
2. The extreme difficulty of discovery.
3. The complexity of reproduction.

For the team behind dqlite, this discovery raised a critical concern:

The Crucial Question: Is dqlite susceptible to this specific corruption bug?

To answer this, we couldn't just guess; we needed to map the exact sequence of events leading to the failure. Our strategy involved using TLA+ to create a formal model of SQLite's behavior, identify a failure trace, and then verify if dqlite's implementation of SQLite allows that trace to occur.

---

Understanding SQLite WAL and Checkpoints

To model the bug, we first need to understand how SQLite handles concurrency. SQLite utilizes a WAL mode to ensure that readers do not block writers.

How it Works

Instead of modifying the main database file directly, writers append changes to a staging area known as the Write Ahead Log. Readers can continue to access the main database, ignoring the new data until it is finalized. Eventually, a checkpoint occurs, where the data from the WAL is migrated into the primary database.

To keep the WAL from growing indefinitely, a writer will attempt to expand reset (overwrite) the log if the most recent checkpoint successfully moved all pages.

Orchestration and Locking

SQLite manages this process using shared memory and specific locks:

Note: The range $[nBackfill+1, mxFrame]$ represents the pages not yet copied to the database.

---

Modeling the Bug in TLA+

The challenge of TLA+ is abstraction: deciding what to include and what to ignore to keep the specification simple yet faithful.

1. Defining the State

We represent the database and WAL using the following variables:

$\text{VARIABLES } wal, db, nBackfill, mxFrame, walSalt$

To simplify the model, we treat each data page as a unique integer.

• The WAL is modeled as a sequence of these integers.
• The Database is modeled as a set of these integers.

Initial State: $\text{Init} \triangleq \langle wal = \langle \rangle, db = \emptyset, nBackfill = 0, mxFrame = 0, walSalt = 0 \rangle$

2. The Modeling Process

Our goal was to simulate the interaction between two primary actions:

• Appending: Adding new pages to the WAL.
• Checkpointing: Moving pages from the WAL to the DB.

3. Analyzing the C Source

To ensure the TLA+ action was accurate, we analyzed the SQLite C code responsible for appending frames (walFrames).

static int walFrames( 
    Wal *pWal, 
    int szPage, 
    PgHdr *pList, 
    Pgno nTruncate, 
    int isCommit, 
    int sync_flags 
){ 
    int rc; 
    u32 iFrame; 
    PgHdr *p; 
    PgHdr *pLast = 0; 
    int nExtra = 0; 
    int szFrame; 
    i64 iOffset; 
    WalWriter w; 
    u32 iFirst = 0; 
    WalIndexHdr *pLive; 

    assert( pList ); 
    assert( pWal->writeLock ); 
    
    /* If this frame set completes a transaction, then nTruncate != 0. */
    assert( (isCommit!=0)==(nTruncate!=0) ); 

    pLive = (WalIndexHdr*)walIndexHdr(pWal); 
    if( memcmp( pWal->hdr, (void *)pLive, sizeof(WalIndexHdr))!=0 ){ 
        iFirst = pLive->mxFrame+1; 
    } 

    if( SQLITE_OK!=(rc = walRestartLog(pWal)) ){ 
        return rc; 
    } 
    // ... further logic for writing WAL header ...
}

In this snippet, the code checks if the shared memory header (pLive) matches the WAL header. If they differ, it calculates iFirst based on mxFrame. This logic is a prime candidate for the race condition we are hunting.