Blog
From the team
Thoughts on verification, formal methods, and AI-generated code.
latest · August 30, 2026 · 6 min read
Curiosity-guided bug discovery
The bugs good testing misses are the ones nobody thought to check for. A developer's hunch about a weak spot is a sharp pointer to one of those gaps, if acting on it is cheap. Our loop makes it cheap: a plain question becomes a scoped, machine-checked campaign the customer approves, and the campaign either proves the guarantee or finds the bug. Here is one question about short disk reads during recovery, and the silent data-loss bug it turned up, filed as turso#8593.
August 21, 2026 · 4 min read
Bringing Aristo to networking infrastructure correctness
We are expanding Aristo, our verification SDK, to networking. As a first demonstration we aimed it at HTTP libraries and found a correctness bug in hyper: a request accepted when it arrives in one piece and rejected when the same bytes arrive in two. Reported upstream, and fixed within three days.
August 17, 2026 · 11 min read
Testing samples time: SQLite's WAL reset bug and the case for proofs
SQLite is tested better than almost any software on Earth, yet it carried the WAL reset data race for sixteen years, because the race is rare in time and testing samples time. Reasoning from the published WAL contract, we located the exact window and turned it into a deterministic test on the real binary: 3.51.2 loses committed writes, 3.51.3 keeps them. The case for formal methods as a source of speed, not a tax on it.
August 7, 2026 · 6 min read
The proof maintenance problem
Turso merged a fix for a crash-safety bug we had reported, and the issue closed automatically. Re-checking the whole model at the fix commit showed the fix was correct but had broken a neighboring durability specification no regression test covered. Keeping the whole proof current as the code changes is the problem Aretta solves.
August 4, 2026 · 8 min read
Why verified software remains elusive
Machine checkers for software have grown stronger for decades, yet uptake in production codebases has stayed low. We ask ourselves: why? To answer, we view verification as a trust-building loop between software developers and the verification infrastructure. The bottleneck, it turns out, is not checker strength but the interface.
July 8, 2026 · 8 min read
How Aristo found a durability bug in Turso
Working with the team at Turso, we found a gap in durability, the one promise a database can least afford to break: a small bug with a sharp consequence, and a good illustration of what Aristo is for. Turso wrote up their own account in 'The Final Boss of Reliability'; this is ours.
March 30, 2026 · 9 min read
We Asked Two AI Agents to Build an LSM Database. Only One Got Database Compaction Right.
We built two LSM databases from the same spec — one with proof guidance, one without. 45 tests found zero bugs. A Verus proof skeleton found a silent data-loss bug in database compaction that testing couldn't reach.
Get new posts by email. No spam, and no more than a few a month.
Prefer a reader? Subscribe via RSS →