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.
Read the note 1 min read