Pavan Nambi used Quint to model the SQLite C API, generate traces, and run them against SQLite. The exercise hardened Turso and surfaced over 10 bugs in SQLite itself.