verification · August 30, 2026 · 6 min read

Curiosity-guided bug discovery

Adwait Godboleverification · aristo · turso · durability · case-study

Contents

Applying verification in a scalable and automated manner has always faced a division of expertise. While developers are best placed to identify most critical parts of their codebase and identify potentially dangerous scenarios, applying formal verification itself has been challenging. You had to write a formal specification, set up a proof harness, perhaps learn a proof language. On the other hand, the formal verification expert often operates on the other end: they are masters of the core technique but pointing at the most critical system component has required closely working with the engineering team, something that does not scale. Our key insight is connecting the developer's intuition for weak spots with the verification expert's technical prowess.

Follow the curiosity#

Aretta's curiosity-guided bug discovery loop enables this connection between the developer who knows where to look and the expert who knows how to verify. The loop has three surfaces: Ask, Campaign, and Finding. In Ask, a developer poses questions about their verification record in plain English: which parts have been modelled, and the set of guarantees checked so far. When the record has no answer, because no guarantee on file covers the question, the question becomes a campaign: a newly scoped piece of modelling and verification work, priced up front and tied to a concrete outcome, a new guarantee added to the record and a verdict on whether the code upholds it. If the campaign finds that a guarantee fails, it produces a finding: a bug, described in plain language, on the developer's dashboard.

The customer sets the direction. They decide which question is worth a campaign, they see the price before approving it. We verify where developers point us, rather than based on our guesswork.

A question about short reads#

For Turso, one of our design partners building a modern rewrite of SQLite in Rust, we can put the following question to the Ask surface:

If a disk read comes up short mid-recovery, could it silently lose data I have already committed?

A disk read can return fewer bytes than requested; correct code checks for this and reads the rest. The danger is a short read during recovery, when the engine reads its write-ahead log to restore committed data after a crash. Mishandled there, committed data can be dropped, with no error raised.

Ask draws its answers from the verification record, the models and proofs we have already built, but sometimes the record has none. Here it covered durability once data is checkpointed, but nothing on it addressed a short read during recovery, before the data is folded into the main database.

We close a gap like this by expanding the modelling and verification, and here that meant a campaign: Verify Turso surfaces I/O errors instead of silently swallowing them, seeded by a lead from the durability work we wrote about earlier.

Reconstruction of the Ask surface with a question and a proposed campaign card. — Fig. 1Illustrative reconstruction. Ask answers from the record today; proposing a campaign from the chat is a capability we are building. The campaign card text, price, and estimate are verbatim from the live system; the question and reply are composed for this illustration.

What the check found#

Once approved, the campaign wrote a machine-checked specification of one guarantee: a failed or short disk read on a durability-critical path must be surfaced, never quietly treated as success. Further it attempted to verify the guarantee against the live engine. The check failed. When injecting a short read at the moment recovery reads the log, the above guarantee was violated. On the other hand, when running the identical fault against SQLite as a control, the guarantee held.

The failure of this guarantee is a consequential data-loss class bug. The database engine keeps recently committed rows in a write-ahead log (WAL). This is a side file it replays at open to restore anything not yet folded into the main database. The write-head log begins with a small header. When the read of that header is fragmented, by even a few bytes, the whole log is read as empty, and every committed row in it is discarded. Moreover, this data loss is silent as the query returns, the process exits 0, and PRAGMA integrity_check, the built-in health check, reports ok.

Terminal reproduction: a faulted reopen returns 0 rows and ok; a clean reopen returns 40 rows. — Fig. 2The reproduction: two reopens of the same committed bytes. With a short read of the log header injected, 40 committed rows read back as 0 and the integrity check still reports ok; with no fault, all 40 return.

What it means#

We reported this data loss bug on the project's public tracker, turso#8593, with a reproduction. The launched campaign is now associated with a result: 1 bug found. Further the test capturing the bug durably persists in CI/CD and re-runs on every later change. Thus, the bug cannot be re-introduced unnoticed.

The finding as the customer saw it, with the link to the upstream issue. — Fig. 3The finding as the customer saw it: the guarantee in plain language, the history of the report, the link to turso#8593, and what the check established: 40 committed rows to 0 under a short read, all 40 back on a clean reopen, all 40 kept by SQLite under the same fault.

The specification behind this bug was not represented in any tests. It surfaced because of a curiousity about one specific scenario of disk behaviour. Asking a plain natural language question rather than a week of harness-building resulted in the bug discovery. This is the whole idea: the most valuable checks are aimed where a developer already suspects a weak spot, so the job is to make aiming them cheap. We add to the verification record one question at a time, guided by where developers think the risk lies.

New posts by email. No spam.