Assay SQL engine · Formal verification

Can AI build a database you can trust?

We're finding out in public. Chapter 1 asked whether AI could build a real SQL engine at all. Chapter 2 asks for more: proof that its answers are right.

Chapter 1 · Oct 6 to 7

Build it

Chapter 2 · Since Oct 8

Prove it

Why a second chapter

Step 0 was simple: is this worth doing, and can it be done at all? About 36 hours after our first recorded commit, the answer was yes, and we started chapter 2 the next afternoon. The fast engine passed 79.98% of all frozen SQLite test records (80.04% non-SQLite maximum), or 99.93% of applicable records, with zero observed wrong answers in that run.

But passing tests only shows that no wrong answer turned up. It can't show none exists, and a database that gets an answer wrong doesn't crash. It hands you a number that looks right. So step 1 is more audacious: prove the answers are right, with machine-checked proofs against a written spec, and grow the share of real SQL that's covered until it reaches the ceiling too.

What would move chapter 2 next

Each pilot record that doesn't count yet stopped at the first thing the proven core can't handle. Fixing one item can uncover the next, so these don't simply add up. They do show where the biggest gains are.

Who moved it

DateChangeOwnerToolsResult

Today this log is updated with each export of the code. Once the repository is public, rows will come from merged pull requests and their checks.

Two ways to move it

Prove more of SQL

Raises the number. It counts only when all of these hold, rechecked from scratch:

  1. The proofs check with zero errors and no skipped or assumed steps.
  2. No existing proven statement got weaker.
  3. A rerun on the same frozen test set finds zero wrong answers.
  4. The result is logged with exact source and evidence hashes.

Add test queries

Makes the test harder and the number more meaningful. It may go down, and that's fine.

  1. Each query's expected answer is checked independently, for example by several engines agreeing.
  2. Added queries form a new, frozen version of the test set.
  3. Coverage is always reported against a named version, so old and new numbers are never mixed.
  4. The GitHub owner of the change is credited in this log.