How Aristo found a durability bug in Turso

Durability is the promise a database can least afford to break. When it tells you a write succeeded, that write has to survive a crash. Everything else sits on top of that one guarantee: your balances, your orders, your audit log.

Working with the team at Turso, we found a case where the guarantee had a gap. It's a small bug with a sharp consequence, and a good illustration of what Aristo is for. Turso have written up their own account, generously and in detail, in "The Final Boss of Reliability"; this is ours.

The bug

Turso can run as a local replica that syncs from a cloud master database. As it commits synced pages, it writes them to disk. But writing to disk isn't the same as making data durable: the operating system can hold your bytes in a cache, and only fsync forces them down to the media. So the property is simple:

A transaction may be reported durable only after its commit frame has reached stable storage via fsync.

On the replica-sync path, that second step was missing. The ordering the property requires, and the ordering the code actually took:

correct   write frame  ──▶  fsync  ──▶  report durable
bug       write frame  ───────────────▶  report durable      (fsync skipped)

So if a crash or power loss lands before that data reaches the disk, a write the database has already acknowledged can be gone on restart: silent data loss, or a corrupted copy of the synced database. No one ever hit it; it was caught first. But it was reachable.

Why it's hard to catch

So why is something reachable so hard to actually catch? Because the bug lives on the failure path. The happy path is flawless: a commit completes, everyone moves on. It only bites if a crash lands in one narrow window, and ordinary testing never goes there. Tests run on healthy hardware, where the power doesn't cut out between two lines of code; you can't unit-test a bug that only exists mid-crash.

So you reach for stronger testing, and Turso has some of the strongest there is. Their Deterministic Simulation Testing drops the whole system into a simulated world and injects crashes and power failures on purpose, precisely to expose bugs like this. It is genuinely excellent, and unlike ordinary tests, it can reach this class of failure at all.

It still didn't find this one, and not because it's weak. Testing, even this kind, works by sampling: it runs the scenarios its generators happen to produce, out of a space of crash timings and interleavings far too large to enumerate. In Turso's words, the generators "were not generating the particular situation" that triggered it. The scenario was reachable; it just wasn't reached. Extensive isn't exhaustive, and that gap is where this bug lived.

How Aristo found it

Aristo starts from intent. You state what a piece of code is supposed to do as a plain-language claim, written right above it:

#[aristo::intent(
    "a transaction is reported durable only after its commit frame is fsynced",
    verify = "full",
    id = "commit_is_durable",
)]
fn commit_dirty_pages_inner(/* … */) { /* … */ }

Three parts: the claim in plain English, an id so it can be tracked as the code changes, and a verify mode. The verify mode is the bridge to how the claim gets checked. neural is a fast, local check: an AI critic reads the code against the claim. full hands the claim to Aristo's backend, the engine that reasons about the states the code can reach, not just the ones a test happens to run.

For a durability claim like this one, full is what matters. The backend looked for any reachable execution in which a transaction is reported durable before its frame is fsynced, and it found one. In minutes, and deterministically: the same answer every time, not a matter of the right random seed. How the backend does that is the part we keep to ourselves; what you see is the claim going in and the exact violating case coming back.

That's the shape of the whole product. You declare intent next to your code, Aristo tells you whether the code can break it, and if the code later drifts from the claim, it says so, before the change ships.

A bug is a spec that didn't hold

What we're really after is a proof: that an acknowledged write survives a crash. You can't establish that in one shot, so the proof breaks it into smaller specs, and those into smaller ones, down to leaves you can check against the code. The tree isn't a checklist written from memory; it's what proving the top spec forces onto the table. Every leaf is there in service of the proof above it.

S   ⟺   A1 ∧ A2
A1  ⟺   B1 ∧ B2 ∧ B3
A2  ⟺   C1 ∧ C2

S   an acknowledged write survives any crash
A1  ack only after the commit frame is on stable storage      (write side)
      B1  frame bytes written to the OS                 ✓
      B2  fsync after the write, before the ack         ✗   ← the bug
      B3  ack issued only after fsync returns           ✓
A2  recovery restores every persisted frame                   (recovery side)
      C1  scan the WAL from the last checkpoint         ✓
      C2  re-apply every frame up to the last commit    ✓

Notice what that buys you. Nobody had to think to test that the replica calls fsync. Proving durability required the obligation "fsync before the ack," so it appeared on the tree on its own, and it was the leaf that came back false. The bug wasn't something we went looking for; it was a spec the proof demanded, and the code didn't hold it.

That's all a bug is here: a spec raised in service of a larger proof, that didn't hold.

(Every split here is an exact ⟺, so a red leaf is a real hole in S, not a dead end in one proof attempt.)

What this doesn't mean

We checked one guarantee: that acknowledged writes survive a crash. We did not verify all of Turso, and we won't imply otherwise. Verification also doesn't replace testing. Tests exercise the real system on real hardware, and Turso's simulation testing will keep finding things a single guarantee can't. The two are complementary; Turso framed it the same way, and that's the honest read. What verification adds is coverage of the failure paths you can't afford to leave to chance.

Try Aristo, and what's next

You can try Aristo today. The core, writing intents and checking them locally, is free and open source, so you can start putting claims on your own code right away. The backend proofs that caught this bug (verify = "full") are what we're onboarding design partners for, and as part of our initial launch we're taking on three or four more. If you're building a database, a storage engine, a consensus layer, or anything where a wrong answer on the failure path is unacceptable, we'd like to hear from you.

We're glad to be working with Turso as they head toward their 1.0 release. Getting durability right is easy to overlook and expensive to get wrong, and a team that goes looking for these bugs before their users do is exactly who you want to build alongside.

Join the waitlist: forms.gle/AYoqpeXJq2YQv57S6

Or reach us directly: hello@aretta.ai