Counterexample Studio

Find the smallest sequence that makes an AI-built data feature silently lie.

Comment

Inspiration

AI can generate implementation code quickly. The harder problem is knowing when plausible code passes ordinary tests and still returns the wrong data without an exception.

Counterexample Studio grew out of six public database-correctness fixes across PowerSync and Rocicorp Zero. The defects were small in code but semantic in impact: signed casts, invalid function arity, division by zero, JSON iteration, newline matching, and UTF-8 ordering. The repeated manual loop suggested a product: start from the intended behavior and automatically search for the smallest replayable witness.

The prior fixes establish the problem. Every executable component in Counterexample Studio was built during OpenAI Build Week.

What it does

Counterexample Studio turns a plain-English data invariant into an end-to-end falsification loop:

  • Codex maps the invariant conservatively to a canonical executable contract and exposes assumptions.
  • A seeded generator creates deterministic state-transition traces.
  • A reference model and target adapter execute identical operations.
  • A differential oracle classifies missing rows, unexpected rows, value drift, ordering drift, error asymmetry, and state divergence.
  • Delta debugging removes irrelevant operations while preserving the failure.
  • A tamper-evident bundle records the contract, seed, trace, observations, fingerprint, and SHA-256 integrity digest.
  • A Vitest exporter turns the minimized witness into a durable regression.
  • A live six-contract matrix runs the shared engine directly in the browser and exports verified evidence JSON.

Live executable contract matrix

The six-row catalog is not a screenshot or precomputed result fixture. Selecting any contract runs its real reference and mutant adapters through the same core engine used by the CLI, generates a deterministic 12-operation failure, minimizes it, creates a SHA-256-bound evidence bundle, replay-verifies the bundle, and exposes the JSON for download.

Re-running a contract with seed 1709 reproduces the same minimal witness and bundle ID. A judge can inspect six distinct semantic failures without installing anything.

Independent proof on published code

The product has two deliberately separate validation layers.

The interactive studio uses a controlled IndexedDB cache defect so the entire workflow is visible: a customer changes from pending to complete, the write succeeds, no exception is thrown, but a stale query still returns that customer. Forty operations collapse to the three-step proof.

The historical verifier then executes two exact published PowerSync npm packages around merged PR #646. It does not recreate the bug:

  • pre-fix package: 5 / 0 -> Infinity
  • post-fix package: 5 / 0 -> NULL, matching SQLite
  • generated trace: 10 operations
  • minimized witness: 2 operations
  • exact npm integrity values and upstream source hashes recorded
  • deterministic command: npm run verify:historical

The hash-bound evidence is checked into the repository and rerun in deployment CI.

How we built it

Counterexample Studio is a TypeScript monorepo:

  • packages/core: contract catalog, reference and target adapters, deterministic generator, differential runner, mismatch taxonomy, minimizer, bundle verification, and regression export.
  • apps/studio: a React/Vite operational lab with a real Dexie/IndexedDB target and the live six-contract matrix.
  • packages/mcp: a local five-tool MCP server with path confinement and no network access.
  • skills/counterexample-studio: a Codex skill that compiles invariants, invokes deterministic tools, and keeps claims bounded to recorded evidence.
  • scripts/counterexample.mjs: the general CLI.
  • scripts/historical-powersync-replay.mjs: the published-package verifier.

Codex coordinated the product decision, architecture, provenance checks, integration, browser QA, and release. GPT-5.6 coding agents implemented disjoint core-engine and MCP/skill slices. The engine is deterministic, offline after installation, and fails closed on malformed or unverifiable artifacts. Canonical hashing uses audited browser-compatible @noble/hashes so Node and browser bundles retain identical SHA-256 semantics.

Challenges we ran into

The hardest design decision was epistemic: a generated test pass is not proof of correctness. The product had to distinguish a verified counterexample, a regression covering one witness, and a bounded run that found no witness. That claim boundary shaped the bundle, UI, MCP annotations, and Codex instructions.

The historical replay also falsified Counterexample Studio itself. It exposed an oscillation in value simplification that could exhaust the minimizer's evaluation budget. We replaced it with a strictly monotonic simplification order and added a regression test. A correctness tool should be willing to find faults in its own machinery.

Accomplishments that we're proud of

  • Six deterministic executable contracts and 384 seeded property cases.
  • Forty-six passing automated tests.
  • Six live browser runs that minimize, hash-bind, replay-verify, and export real evidence without fixture JSON.
  • A precise mismatch taxonomy and bounded delta-debugging minimizer.
  • Tamper-evident evidence bundles with deterministic replay.
  • Runnable Vitest regression export.
  • A real IndexedDB target demonstration.
  • An independent before-and-after replay of a genuine merged upstream defect.
  • Local Codex skill and MCP integration with explicit trust boundaries.
  • Clean TypeScript/build validation, zero npm audit findings, and historical verification in Pages CI.

What we learned

The highest-leverage use of an AI coding agent is not merely generating more implementation. It is turning intent into an adversarial, inspectable test loop. The useful output is not a confident sentence. It is a small witness another engineer can replay.

What's next for Counterexample Studio

  • Adapter SDKs for SQLite, Postgres, sync engines, and application caches.
  • Contract synthesis from schemas, existing tests, and issue descriptions.
  • Stateful coverage guidance across multiple seeds.
  • CI annotations that attach the minimized witness and generated regression to a pull request.
  • A versioned corpus of public semantic-compatibility contracts.

Try it

Built With

Share this project:

Updates