Formal verification caught bugs SQLite's test suite missed
Turso used a TLA+ variant called Quint to model their libSQL fork and found over ten real bugs in SQLite's transaction logic that billions of existing tests never saw.
Turso hardened their libSQL fork and found over ten bugs in SQLite’s transaction handling. Not in libSQL’s changes. In SQLite itself. Using formal verification, not fuzzing. SQLite has 711 times more test code than implementation code. It has been in production for decades. Billions of devices run it. The test coverage is famous. But Turso’s team wrote a formal model in Quint, a variant of TLA+, and the model checker found edge cases in BEGIN IMMEDIATE and SAVEPOINT interactions that no test ever hit. The bugs were real. Turso reported them upstream. SQLite fixed them. The test suite did not catch them because the coverage was wide, not exhaustive. You can have a million tests and still miss the one specific interleaving that breaks isolation. Formal verification tools explore state spaces systematically. You define what correct behaviour looks like in mathematical terms, and the checker tries every possible execution path within the model’s scope. It is slow. It is annoying to write. But it finds things that random inputs and manual scenarios do not. Quint is interesting because it compiles TLA+ style specs into executable code. You can run the model against real system traces. Turso did that. They modelled their replication protocol, checked it against the SQLite transaction semantics, and the checker flagged violations. This is not replacing tests. It is a second opinion for the critical paths. If your system has transaction ordering, consensus, or lock interactions, model checking might be worth the setup cost. SQLite’s test suite is the gold standard, and formal methods still found bugs it missed.
Source: We used Quint to find over 10 bugs in SQLite while hardening Turso