6. Bonus: How was the bug fixed in SQLite?

On March 5, 2026 SQLite disclosed the bug and published a fix. A single extra check is enough to avoid the data race by checking that a reset of the WAL did not occur since we started the checkpoint: SQLite code that fixes the bug WalIndexHdr *pLive = (WalIndexHdr*)walIndexHdr(pWal); /* Now that read-lock slot 0 is locked, check that the wal has not been ** wrapped since the header was read for this checkpoint. If it was, then ** there was no work to do anyway. In this case the ** (pInfo->nBackfill hdr. mxFrame) test above only passed because ** pInfo->nBackfill had already been set to 0 by the writer that wrapped ** the wal file.

It would also be dangerous to proceed, as there may be ** fewer than pWal->hdr. mxFrame valid frames in the wal file. */ int bChg = memcmp(pLive->aSalt, pWal->hdr. aSalt, sizeof(pWal->hdr. aSalt)); if( 0==bChg ){ pInfo->nBackfillAttempted = mxSafeFrame; SEH_INJECT_FAULT Checkpoint ≜ ∧ checkPointState = waitingForLock" ∧ IF walSalt = pWalSalt THEN \* Move pages from wal into db.

∧ db' = db ∪ { wal[j] : j ∈ nBackfill+1‥Len(wal) } ∧ nBackfill' = safeMxFrame ELSE \* Salt changed, we skip the checkpoint. ∧ UNCHANGED ⟨ nBackfill, db ⟩ \* Reset the checkpoint state. ∧ safeMxFrame' = 0 ∧ pWalSalt' = 0 ∧ checkPointState' = notStarted" ∧ UNCHANGED ⟨ mxFrame, wal, pageNumber, walSalt, writeLock ⟩ Running the model-checker for the TLA+ model with the same invariant returns no error now, confirming the fix.