#testing

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 post ↗