Equividence

Your migration passed. Your promise didn’t, Equividence finds the smallest SQLite database that proves it.

Comment

Equividence

Your migration passed. Your promise didn’t. Equividence finds the SQLite database that shows why.

Inspiration

We kept coming back to a frustrating class of database bug: the migration succeeds, but the application is wrong afterward.

Our demo starts with a two-row case. The customer records have contacts that differ only by letter case. A migration lowercases those contacts into a unique column and uses INSERT OR IGNORE. SQLite runs the statement without error. One customer survives; the other quietly disappears.

The database did exactly what the SQL requested. The migration still broke the requirement the developer cared about: every historical chargeback must continue to resolve through its original customer ID.

That distinction became the project. Let the source database be S, the migration be M, and the promised behavior be I. Equividence looks for a concrete witness database where:

$$M(S^{\star})\downarrow\;\land\;\neg I(S^{\star},M(S^{\star}))$$

In other words, the migration executes and the requirement fails. We wanted the result to be a database a developer could run, inspect, and keep as a regression.

What it does

Equividence is a counterexample compiler for SQLite migrations.

The developer provides three things:

  1. The current SQLite schema
  2. The migration SQL
  3. A short description of what must still be true afterward

GPT-5.6 reads a bounded representation of those inputs and proposes a typed challenge. Its proposal includes the relevant source spans, the suspected risk, a generator recipe, and an invariant that can be reviewed. The developer can edit that invariant or reject it. Nothing executes until the invariant is explicitly approved.

Once approved, SQLite runs inside a browser Worker. Equividence generates candidate rows, applies the real migration, and checks the approved invariant. When it finds a failure, it removes unnecessary rows and runs the surviving case again in fresh databases.

The final receipt includes:

  • The rows before and after the migration
  • The exact invariant that failed
  • Replay SQL containing the schema, fixture, and migration
  • A dependency-free Node regression test
  • A JSON evidence receipt with fingerprints for the proposal, human contract, submitted program, and execution result

The receipt supports one precise claim: this database violates this approved invariant under this SQLite execution. The scope ends with that witness and invariant; broader safety remains unproven.

How we built it

The main architectural decision was to keep proposal, authorization, and execution separate.

GPT-5.6 handles the part that benefits from semantic reasoning. It connects the developer’s requirement to concrete pieces of the schema and migration, then returns strict structured output. The API validates every referenced table, column, span, and challenge type before the proposal reaches the interface.

The developer owns the contract. Approval is tied to the exact schema, migration, and invariant on screen. Editing any of them clears the approval and any evidence derived from it.

SQLite owns the result. A Web Worker runs SQLite WASM, generates typed rows, applies the submitted migration, evaluates the invariant, shrinks the witness through row deletion, and replays it in clean databases. Executable fixtures, assertions, and verdicts come from deterministic code.

The product is built with TypeScript, React, Vite, Node.js, Express, SQLite WASM, Web Workers, Zod, Vitest, and Docker. We used OpenAI Codex throughout the build to trace failure paths, refactor the engine boundary, write adversarial tests, review the security model, and keep the public documentation synchronized with the implementation.

The public GitHub Pages build uses checked-in GPT-5.6 planner output for its bundled examples because a static site cannot safely hold an API key. The SQLite generation, migration execution, shrinking, and replay still happen live in the browser. The server-backed build uses the OpenAI Responses API for live planning.

Challenges we ran into

The hardest problem was turning a human requirement into something executable without pretending that the model had discovered the requirement on its own. “Customers must remain resolvable” sounds clear to a person, but an engine still needs to know which rows are in scope, which identity matters, and what counts as preservation. Making that contract visible and editable was more important than adding another autonomous step.

Shrinking the failure took more work than finding it. A large generated database can expose a bug while still being unpleasant to understand. Our shrinker repeatedly removes rows, rebuilds the database, reruns the migration, and keeps a deletion only when the same invariant still fails. Fresh replay confirms the minimized witness in clean databases.

We also had to be strict about unsupported SQL. Triggers, attached databases, environment-dependent pragmas, nondeterministic functions, and other operations can escape the assumptions of the local engine. Those cases stop before execution and explain why.

Our first evaluation corpus also taught us an uncomfortable lesson: a benchmark can flatter the system that authored it. We found leakage in an early version, kept the failure visible, rebuilt the corpus, and added holdout cases, malformed responses, unsupported inputs, causal pairs, and a regression based on Django ticket #29182.

Finally, the static public demo required an honest boundary. We chose to label recorded planner responses clearly while keeping the part that produces evidence—the SQLite run—fully live and inspectable.

Accomplishments that we're proud of

  • A complete executable path. The product goes from schema and human requirement to an approved invariant, minimized witness, replay, and regression artifact.
  • A clear authority boundary. GPT-5.6 proposes the challenge, the developer approves the contract, and SQLite determines whether the witness fails.
  • Portable evidence. The exported SQL and Node test can leave the interface and become part of an ordinary debugging or CI workflow.
  • A useful causal control. Two bundled cases use byte-identical SQL while changing only the human promise, showing that the requirement genuinely changes the verdict.
  • An external regression. The Django #29182 case checks the same engine against a documented SQLite migration failure outside our own examples.
  • Reproducible validation. The checked-in corpus contains 15 contract cases, 45 planner trials, and 9 fresh witness replays. The repository currently has 100 passing tests, with three environment-dependent tests skipped on unsupported Node versions.
  • Honest failure behavior. Invalid model output and SQL outside the supported boundary are rejected with a specific explanation.

What we learned

The application requirement is part of the migration specification, even when it exists only in a developer’s head or a ticket. Schema comparison alone cannot recover it reliably.

We also learned that a language model is most useful here as a bridge between that requirement and a testable structure. The final evidence becomes much stronger when another system can reproduce it without asking the model to agree with itself.

Small counterexamples matter. The two-row witness in our demo explains the failure faster than a long review comment could. It also gives the developer an immediate regression test for the eventual repair.

That led to another lesson: uncertainty belongs in the product. Equividence states what each receipt establishes, records where its proposal came from, and stops when the deterministic engine cannot support the requested challenge.

What's next for Equividence

The current version focuses on SQLite migrations and a bounded set of preservation invariants. The next useful steps are:

  • Add invariant families for value preservation, reachability, scoped uniqueness, aggregates, and richer referential relationships
  • Import migrations directly from repositories and common TypeScript migration frameworks
  • Run Equividence in CI and attach the minimized witness and regression file to a pull request
  • Compare behavior across SQLite versions and alternative migration implementations
  • Build a reviewed library of invariant templates and retain developer corrections as evaluation data
  • Track each promise, witness, repair, and regression result as a durable project artifact

Our goal is to make preservation promises executable and keep them beside the migrations they protect.

Built With

Share this project:

Updates