Hardening Turso: Finding SQLite Bugs with Formal Methods and Quint

For any team building a database, SQLite represents the gold standard for reliability. Because Turso is a rewrite of SQLite, maintaining that same level of trust is not just a goal—it is a necessity. To achieve this, Turso employs a rigorous testing stack including Deterministic Simulation Testing (DST), differential testers, fuzzers, and concurrency simulators.

Despite this comprehensive approach, the team recognized a gap in their strategy: formal methods. While traditionally viewed as inaccessible or overly complex, formal methods provide a mathematical certainty that traditional testing cannot. By integrating Quint, a modern tool for formal verification, Turso was able to push their hardening process further, ultimately discovering over 10 bugs within SQLite itself.

The Challenge of Formal Methods

Formal methods, such as TLA+, are the industry benchmark for verifying system correctness. However, they often suffer from a high barrier to entry and the "who watches the watchmen" problem—the difficulty of verifying that the model of the system is actually correct.

To overcome this, Turso collaborated with community member Pavan Nambi to utilize Quint. Quint combines the theoretical foundations of the Temporal Logic of Actions (TLA) with modern type checking and development tooling, making it more accessible to engineers.

Rather than attempting the impossible task of modeling the entire SQLite system, the team focused on the C API. Since the C API is well-documented and serves as the primary interface for most SQLite drivers, modeling it provided a high-leverage point for coverage. This approach allowed the team to use the API specification as a source of truth to verify both the model and the actual implementation.

The "Quinting" Process

The methodology for finding bugs was a repetitive, four-step cycle:

1. Model the Contract: Identify a documented SQLite C API contract and model the necessary state and properties in Quint.
2. Generate Traces: Use Quint to generate a sequence of states (traces) that could potentially violate the contract.
3. Execute: Translate these traces into a small C program and run them against SQLite.
4. Compare: Compare the observed behavior of the system against the documented result.

When the model checker identifies a failure, it produces a counter-example—a specific sequence of states that leads to the violation. While many of these counter-examples simply validated that the model was correct, others revealed that the system was deviating from its own specification.

Case Study: sqlite3_deserialize()

One prominent example involved the sqlite3_deserialize() function, which allows a serialized database image to be loaded into a connection as an in-memory database.

According to the specification, sqlite3_deserialize() should return SQLITE_BUSY if the target database is currently in a read transaction or involved in a backup operation. The Quint model generated a trace with the following sequence:

1. Open database $\rightarrow$ Create table $\rightarrow$ Serialize database.
2. Start reading from the database.
3. Call sqlite3_deserialize() while the read transaction is active.

While the expectation was a SQLITE_BUSY return code, the actual result was a system crash. Because crashes are almost never the intended behavior, this provided immediate confirmation that the bug existed in the implementation, not the model. This issue was subsequently fixed in the SQLite source.

Results and Findings

The exploration with Quint was highly productive, uncovering a wide array of bugs ranging from logic errors in optimizations to critical crashes. Key findings included:

• Optimization Failures: Issues where EXISTS-to-join optimizations incorrectly applied LIMIT/OFFSET or lost outer correlation, filtering out valid rows.
• Constraint Violations: Bugs where quoted constraint names became undroppable or where xfer optimizations bypassed check constraints, leading to inconsistent databases.
• Stability Issues: Crashes occurring during ALTER ADD CHECK on internal tables or NULL pzErr crashes in sqlite3changegroup_change_finish().
• Memory and Alignment: Undefined behavior related to sqlite3_mutex 128-byte alignment.

Conclusion

SQLite is one of the most thoroughly tested pieces of software in existence. Yet, by applying formal methods through Quint, Turso was able to find bugs that had evaded decades of traditional testing disciplines.

By translating formal traces into executable C programs, Turso not only hardened its own implementation but contributed significantly to the stability of the wider SQLite ecosystem. This demonstrates that formal methods, when applied to specific, well-defined interfaces like a C API, are a powerful tool for modern software reliability.