blog

From the team

July 8, 2026verificationaristodurabilitycase-studyturso

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, 2026verificationformal-methodsaicase-studylsm-tree

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.