On June 25, 2026, a technical blog post quietly went up on Ubuntu’s website. The headline contained two facts that shouldn’t be able to coexist: SQLite — the most widely deployed database engine on the planet — was found to have a bug. And that bug had been sitting in the code since 2010.
Sixteen years.
What does sixteen years mean, in context? In 2010, the iPhone 4 had just launched. WeChat didn’t exist yet. People were still texting on T9 keypads. And that year, a single line of code was committed to SQLite, and the bug came with it. From that moment on, it quietly lived inside every smartphone, every browser, every operating system. Billions of devices. Sixteen years. Nobody ever found it.
And in the end, it wasn’t a human who caught it. It was a math problem.
Figure: Ubuntu’s team used TLA+ to model SQLite WAL checkpoint behavior. The model reproduces the 16-year-old bug in just 20 steps. Source: ubuntu.com
First, Let’s Get One Thing Clear: What Is SQLite, and Why Is It on Your Phone?
SQLite is not an “app.” You won’t find an icon labeled “SQLite” on your phone. It’s a database engine — a piece of software that stores and manages data inside your phone, your computer, your browser.
Here’s a concrete example: your WeChat message history. Your phone’s contact list. The passwords saved in your browser. The local data generated by Alipay, Taobao, TikTok — behind almost all of it, SQLite is quietly doing the work. It is the single most-installed database engine in existence. Estimates suggest over one trillion SQLite databases are running worldwide.
So when a piece of foundational software like this turns out to have had a bug in it for sixteen years, the thought alone is enough to send a chill down your spine.
But the truly remarkable part of this story isn’t the bug itself. It’s how it was found.
A Problem That Was Doomed to Be Invisible to Humans
Let’s look at the bug itself. SQLite has a mode called WAL — Write-Ahead Log. The rough idea: when multiple programs read from and write to the database simultaneously, WAL acts as a scratch buffer. Writers write to the buffer first; readers stay unaffected. When the write is done, the buffer gets merged into the main database file. This merge process is called a “checkpoint.”
The bug lives in the space where “merging” and “writing” happen at the same time. Here’s an analogy:
Imagine you and a colleague are working on a shared spreadsheet. Your colleague is appending new data to a “draft section.” Your job is to take confirmed entries from the draft section and copy them into the official file. You scan the draft section, see 100 records to move, and start copying — you move 50. At that exact instant, your colleague appends 5 more records and “resets” the draft section’s counter. You continue copying the remaining 50 records, but because the counter was reset, you’re actually copying stale indices — and some records that genuinely should have been moved are left behind.
The result: the official file is missing entries. Data loss.
This is the bug described in SQLite’s official documentation: a race condition in the WAL checkpoint process — two operations with no coordination, colliding in a vanishingly small time window.
The key word is “vanishingly small.” Triggering this bug requires a precise chain of conditions: a write operation and a checkpoint operation must overlap. Between the moment the checkpoint reads the WAL size and the moment it starts moving data, another write must complete and reset the WAL — all within a window measured in microseconds.
When humans write test cases to find bugs, they’re essentially guessing. You guess where things might break, then poke at it repeatedly. But this bug’s trigger window is so narrow it falls into the category of “you’d never even think to guess it.” No matter how many testers you hire, no matter how many automated test scripts you write, you cannot cover every possible interleaving of operations — because the number of possible combinations is astronomical.
That’s why this bug lived peacefully inside billions of devices for sixteen years.
What Is TLA+? Not Testing Software — Mathematical Proof
To understand how Ubuntu’s team found this bug, you need to understand one concept: formal verification.
Here’s the simplest analogy I can offer: traditional testing is like spot-checking — you reach into a sack of rice, grab a handful, and see if there’s any sand. Formal verification is like a mathematical proof — you can logically derive whether there is sand in the sack at all, without sifting through every grain.
TLA+ is a formal verification tool. The name stands for Temporal Logic of Actions. It was created by Leslie Lamport, a legend of computer science — the same person who invented LaTeX (the academic typesetting system) and designed the Paxos consensus algorithm (the foundation of nearly every distributed system today).
What TLA+ does is straightforward in principle: you abstract the software behavior you want to check into a mathematical model. You don’t write code. You use mathematical language to describe “how this thing should change under different circumstances.” Then TLA+‘s model checker exhaustively explores every possible state combination and verifies whether the rules you defined always hold.
In the Ubuntu team’s own words: after they built the TLA+ model of SQLite’s WAL behavior, the model checker “found a counterexample in just 20 steps.” Twenty steps. Sixteen years versus twenty steps.
Figure: A static rendering of the TLA+ model showing how the race condition between write and checkpoint operations leads to data loss. Source: ubuntu.com
Why Human Eyes Can Never Win This Fight
There’s a deeper question here worth unpacking: why can a mathematical method find a bug that escaped detection for sixteen years? The answer lies in a fundamental difference of methodology.
Human testing — whether it’s manual clicking or automated scripts — is fundamentally enumerative: you list some scenarios you think might break, and you verify each one. The problem is that a software system’s state space explodes combinatorially. A system with 100 steps has a number of possible state orderings equal to 100 factorial — a number larger than the atoms in the observable universe. You cannot enumerate them all.
TLA+ and similar formal verification tools, while not immune to “state explosion” in theory, do one thing humans cannot: they check: under all the conditions I’ve defined, can a problem occur?
That sentence deserves a second read.
Human testing answers the question: “What problems do I see?” Formal verification answers the question: “Is it possible for a problem to occur?”
The first is passive, dependent on imagination, and leaky. The second is active, exhaustive, and will not miss a single computed state.
The Ubuntu engineers were not smarter than the SQLite developers. SQLite’s development team is legendary for code quality, and its test suite coverage is among the best in the industry. But tools matter. A ruler and a microscope don’t see the same world.
Why the Competitor Wasn’t Affected: A Serendipitous Discovery
There’s an interesting side story here. The reason Ubuntu’s team ran this verification in the first place is that they maintain their own project called Dqlite — a distributed database built on top of SQLite. They wanted to know: does SQLite’s bug also exist in Dqlite?
So they built a second TLA+ model, this time for Dqlite. The result: Dqlite is not affected.
The reason is simple: Dqlite’s design is more conservative. During checkpointing, Dqlite locks out all write operations, ensuring that “merge” and “write” cannot overlap. This costs some performance, but it happened to sidestep the race condition entirely.
Dqlite’s design isn’t necessarily “better.” But sometimes a conservative choice you make without much thought is vindicated sixteen years later. The causal chains in software engineering work in strange ways.
SQLite’s Fix: One Line of Code
On March 5, 2026, SQLite’s team released the fix. It is remarkably simple: during a checkpoint, add one extra check to confirm that the WAL hasn’t been reset. If it has, start over.
Sixteen years of latent risk, resolved with a single line of code.
But the simplicity of the fix doesn’t mean the problem was simple. Knowing where to put that line — knowing what condition to check — that was the truly hard part. Hard enough that some of the best database engineers in the world didn’t spot it for sixteen years.
What This Means: A Trend That’s Changing the Industry
Two points I want to make.
First, the SQLite case is not an isolated incident. Amazon, Microsoft, Oracle, and others have been using TLA+ for formal verification of critical infrastructure for years — AWS services like S3 and DynamoDB went through TLA+ model checking in early design stages. But most of those cases happened inside closed corporate systems, invisible to the public. SQLite, as a ubiquitous open-source project, having a bug found through formal verification, is a landmark event with public visibility.
Second, the barrier to formal verification is coming down. TLA+ is not a tool for casual users — it requires mathematical thinking and systems modeling ability. But twenty years ago, nobody thought “automated testing” was something every team should do; today it’s table stakes. Formal verification is on the same trajectory: moving from “wizard-only” to “team standard.” The fact that Ubuntu’s team used TLA+ to find a bug in the most mature, most widely deployed database in the world sends a signal: the foundational software you trust may contain problems even its authors don’t know about. And mathematics is the only reliable way to find them.
Sixteen years ago, people tested software with intuition and diligence. Sixteen years later, a math problem found, in twenty steps, a bug that human eyes would never have seen.
That’s not a story about people getting better. It’s a story about tools getting better.
Reference links: