A 16-Year-Old SQLite Bug Was Caught by Math, Not AI

There is a piece of software almost certainly running on the device you’re reading this on right now. It’s called SQLite. It ships in your phone, your browser, even aircraft systems — with more than one trillion deployments, it’s the most widely installed database on Earth. And in this software, tested and re-tested to near-mythical standards, someone just found a bug that had gone unnoticed for 16 years. The most interesting part isn’t the bug. It’s how they found it: not with a shiny AI coding tool, but with a mathematical formal verification technique that dates back to the 1990s.

The Bug That Hid for 16 Years

The stage for all this is SQLite’s WAL, or Write-Ahead Logging, mode. WAL is a scheme where changes aren’t written straight into the database. Instead they’re recorded first in a separate log file. It’s a big performance win, but the logic is genuinely tricky, because multiple processes can read and write at the same time and the data has to stay consistent through all of it.

The bug that surfaced lived in a boundary condition around WAL’s checkpoint process. It only appeared when specific operations overlapped in a specific order at a specific moment — a rare race condition. Under normal use it almost never fires. But when it does, data can silently drift out of sync. Hard to spot, potentially catastrophic. The worst kind.

Here’s the punchline. SQLite is used by hundreds of millions of people and is famous for test coverage approaching 100 percent. And even there, human eyes and ordinary tests missed this for 16 years.

The Real Break Came from dqlite and TLA+

The bug came to the surface through a project called dqlite. dqlite is an extension that lets you run SQLite across a distributed cluster. Because it replicates data across multiple servers, its authors had to understand and model the original SQLite WAL behavior with extreme precision.

The tool they reached for was TLA+. TLA+ doesn’t run your code. It’s a formal specification language that defines every state a system can reach and then checks those states mathematically. It was created by Turing Award winner Leslie Lamport, and it’s well known as the tool Amazon uses to design large-scale distributed systems.

If a normal test asks “given this input, do I get this output?”, TLA+ asks “across every state this system could possibly reach, is there even one that’s wrong?” The machine walks through timing combinations no human would ever imagine. That exhaustive sweep is exactly what caught a race condition that had slipped through the testing net for 16 years.

Why This Story, Why Now

Let’s be honest: formal verification isn’t new. In academia it’s practically old-fashioned. So why is this story suddenly getting so much attention? Because of the moment we’re in.

We now live in an era where AI produces code like a firehose. The volume a single developer generates and reviews in a day dwarfs what it was a few years ago. And here’s the catch: the more code you produce, the smaller the fraction a human can actually verify. If AI writes plausible-looking code that quietly breaks on a subtle boundary condition, who catches it, and how?

This is exactly where formal verification gets summoned back. As “make lots of it” gets cheaper, “prove it’s actually correct” gets relatively more valuable. If you can generate code ten times faster, the means to guarantee that code is right matters ten times more. The SQLite case is a near-perfect symbol of that argument.

It’s Not a Silver Bullet

To be fair, there’s a cold-eyed side to this too. Worth noting up front: community discussion on this topic over the past 30 days has been thin, so this piece leans on the substance and context of the technology rather than the online buzz.

Formal verification like TLA+ has a steep barrier to entry. Translating a system into a mathematical specification is a specialized skill in its own right. You can’t just bolt it onto any project. And it verifies whether you built the thing to spec — not whether the spec itself is correct. There’s always a gap between the model and the real code.

So the realistic picture is this. Formal verification doesn’t replace all your tests. It’s a precision instrument, deployed selectively on the concurrency-tangled core logic — the WAL-shaped parts. Expensive and hard, yes. But used properly, it finds things people miss for 16 years.

The Takeaway

The message here is clear. The ability to produce code fast and the ability to prove that code is correct are two entirely different problems. The harder AI pushes the productivity axis forward, the more the value of old mathematics — the thing holding down the verification axis — paradoxically shines.

So ask yourself: is your team spending its resources on how fast you ship code, or also on how certain you are that it’s right? How you balance those two might turn out to be the real fault line dividing good software from the rest.