Equividence

A counterexample compiler for SQLite migrations.

Equividence turns a developer-written preservation promise into a small, replayable database that breaks it.

A migration can return success while silently dropping an identity, duplicating a row, changing a value, or leaving a foreign key pointed at a dead table. Equividence looks for concrete evidence of that kind of failure. It does not label a migration safe.

• Track: Developer Tools
• Live demo: shuv-amp.github.io/Equividence
• Source: github.com/shuv-amp/Equividence

_{Recorded planner proposals; SQLite execution, shrinking, replay, and artifact generation run live in the browser.}

The proof in 20 seconds

The main demo uses a migration that normalizes customer contacts with lower(), UNIQUE, and INSERT OR IGNORE.

The migration succeeds. The preservation promise fails:

2 required customer identities  →  1 migrated identity
missing identity                →  102
fresh replay                    →  reproduced twice

Equividence exports the failing database as:

• replayable SQL;
• a dependency-free Node regression test;
• a JSON evidence receipt with separate model, human, program, and SQLite records.

How it works

flowchart LR
    subgraph DEFINE["1 · DEFINE"]
        direction TB
        A["Schema + migration"] --> B["Preservation promise"]
        B --> C["Deterministic extraction"]
    end

    subgraph AUTHORIZE["2 · AUTHORIZE"]
        direction TB
        D["GPT-5.6 proposes<br/>a typed challenge"] --> E["Server validates<br/>every reference"]
        E --> F["Developer confirms<br/>the exact invariant"]
    end

    subgraph EXECUTE["3 · EXECUTE"]
        direction TB
        G["SQLite WASM runs<br/>the migration"] --> H["Shrink + replay twice"]
        H --> I["Replay SQL · Node test<br/>evidence receipt"]
    end

    C --> D
    F --> G

Loading

The authority boundary is deliberate:

Authority	May do	May not do
GPT-5.6	Propose a bounded risk, cite source spans, and select a typed recipe	Write executable SQL, witness rows, assertions, or the verdict
Developer	Accept, edit, or reject the exact invariant	Keep approval after changing the invariant
SQLite engine	Generate rows, execute the submitted migration, evaluate, shrink, and replay	Expand beyond the supported contract

The model frames the question. The developer owns the contract. SQLite produces the evidence.

Product flow

1. Define — paste or import a source schema and migration, then state one preservation promise.
2. Analyze — deterministic extraction creates exact spans and opaque IDs; GPT-5.6 returns a strict typed proposal.
3. Confirm — inspect the cited SQL, assumptions, identity mapping, and invariant. Rejecting runs nothing.
4. Compile — a fresh browser Worker loads official SQLite WASM and creates bounded source rows with prepared statements.
5. Prove — SQLite runs the real migration, a deterministic oracle evaluates the invariant, and row deletion shrinks the witness.
6. Export — download replay SQL, a Node regression, and an evidence receipt.

Controlled examples

Case	What changes	Result
Chargeback lookup	Contacts are case-folded while legacy IDs must survive	Two-row identity-loss witness
Canonical identity	The SQL is byte-identical, but the promise retires legacy IDs	No authorized challenge; not a safety claim
Django #29182	A table rebuild retargets a child foreign key to a temporary table	One-parent, one-child regression witness

The first two cases isolate the human requirement: suspicious syntax alone does not decide failure.

Quick start

Requirements

• Node.js 22 or newer for the product;
• Node.js 24 for the root benchmark and generated Node regression;
• npm 10+ and pnpm 10.28.2;
• a modern browser with WebAssembly and Web Workers;
• an OpenAI API key for live analysis.

Run the product

Run these commands from the repository root:

cd product
npm ci
cp .env.example .env

Set these server-side values in product/.env:

OPENAI_API_KEY=replace-locally
EQUIVIDENCE_SAFETY_SALT=replace-with-at-least-32-random-characters

Then start both the web app and API:

npm run dev

Open http://localhost:5173.

For an offline walkthrough of the unchanged bundled cases:

EQUIVIDENCE_DEMO_FALLBACK=1 npm run dev

Recorded mode is visibly labeled and refuses edited input. It is not a live model run.

Validate

Run these commands from the repository root in a new shell:

# Root benchmark and contracts
pnpm install --frozen-lockfile
pnpm typecheck
pnpm test
pnpm exec tsx src/cli/v3-verify-public-evidence.ts

# Product tests and production build
cd product
npm ci
npm run preflight

The latest Node 24.14 run completed 112 tests: 24 root tests and 88 product tests passed with no skips. The production bundle also built successfully.

The tested public path is a current desktop Chromium browser with WebAssembly and Web Workers. The live server and static hosted walkthrough were exercised on macOS; other browser and operating-system combinations are not yet claimed as tested.

Hosted walkthrough

The public GitHub Pages walkthrough runs without a backend:

• frozen GPT-5.6 proposals are visibly labeled Recorded analysis;
• only unchanged bundled cases are accepted;
• edited input is rejected rather than presented as analyzed;
• SQLite WASM execution, shrinking, replay, and artifact generation remain live in the browser;
• no API key is shipped to the client.

Build that form locally:

cd product
VITE_EQUIVIDENCE_STATIC_DEMO=1 \
VITE_BASE_PATH=/Equividence/ \
npm run build

The deployment workflow is pages.yml. The project currently uses GitHub's HTTPS project domain. See docs/DEPLOYMENT.md.

Why this is not a model wrapper

Most of the implementation is deterministic:

• source-span, identifier, and literal extraction;
• strict Structured Output and semantic validation;
• a closed recipe and invariant type system;
• same-origin, size, rate, and concurrency controls;
• official SQLite WASM inside a terminable Worker;
• prepared row insertion and SQL authorizer rules;
• progress deadlines and hard Worker termination;
• deterministic invariant evaluation;
• row-deletion shrinking and two clean replays;
• portable artifact generation and receipt verification.

GPT-5.6 is useful because a preservation promise is semantic. The same SQL can be acceptable or broken depending on what the application promises its users. Once a developer confirms that promise, the evidence path no longer depends on model judgment.

Codex collaboration

The dated commit history and implementation record support this summary of how Codex contributed.

Codex helped:

• compare project directions and reject the original assessment-accessibility concept;
• read official rules, migration tools, database papers, and historical bugs;
• design three preregistered evaluation gates before the product build;
• implement the extractor, transport validator, Worker compiler, shrinker, artifacts, and interface;
• find approval-state, transport, scope, and deployment failures;
• run unit, browser, build, container, and claim-integrity checks;
• prepare the product documentation and demo sequence.

The human retained the decisions that matter:

• choose Developer Tools and keep the prototype SQLite-only;
• require explicit human authorization before execution;
• prohibit model-authored executable evidence;
• reject “safe,” “verified,” “certified,” and accuracy claims the evidence cannot support;
• prioritize one visible causal proof over broad feature coverage.

At runtime, GPT-5.6 receives bounded structured evidence and returns only a typed challenge proposal. It does not execute SQL or approve its own result.

Evaluation

The repository contains three kinds of evidence:

1. Automated implementation tests for extraction, transport validation, scope refusal, Worker behavior, artifacts, and red/green regressions.
2. A frozen synthetic benchmark used to test whether the planner adds replayable findings beyond a static baseline.
3. An external repair-paired case derived from Django ticket #29182 and its accepted repair.

The synthetic benchmark is not production accuracy evidence. One historical bug is not a representative corpus. See docs/EVALUATION.md for the exact boundary.

Scope

Equividence currently supports a bounded subset of SQLite migrations and a closed set of executable challenge families:

• normalization and trimming collisions;
• null-sentinel collisions;
• lossy integer transforms;
• simple filter-boundary omissions;
• join multiplicity;
• unexpected identity merges;
• foreign-key retargeting.

It intentionally refuses triggers, views, virtual tables, extensions, attached databases, recursive SQL, nondeterministic functions, arbitrary pragmas, and unsupported syntax.

Equividence is not:

• a migration runner for production databases;
• an automatic migration repair tool;
• a PostgreSQL or MySQL analyzer;
• a proof of universal correctness;
• a certification service;
• a confidence-score dashboard.

Repository guide

Path	Purpose
product/	Runnable React, Express, and SQLite WASM product
src/	Frozen benchmark, planner contracts, and deterministic evaluation engine
benchmark/	Fixtures, schemas, sanitized outputs, and decisions
docs/ARCHITECTURE.md	Components, trust boundaries, and request lifecycle
docs/EVALUATION.md	Reproduced results, evidence levels, and limitations
docs/DEPLOYMENT.md	Live and no-backend hosting paths
docs/CLAIMS.md	Supported claims and evidence boundaries
docs/EXTERNAL_DJANGO_29182_CASE.md	Provenance for the external repair-paired regression
docs/RESEARCH.md	Prior work and primary-source ledger
SECURITY.md	Security posture and reporting
THIRD_PARTY_NOTICES.md	Direct dependency licenses

Current status

• The source repository is public under the MIT license.
• The no-backend walkthrough is deployed over HTTPS.
• The Pages workflow runs the product tests before publishing.
• The hosted walkthrough uses recorded, labeled planner proposals and live browser-side SQLite execution.
• Live GPT-5.6 analysis remains available through the Express deployment when a server-side OpenAI API key is configured.

License

Equividence is available under the MIT License. Third-party components keep their own licenses.