ProofReplay

Turn a human-approved invariant into a live GPT-5.6-authored counterexample, exact replay, test-first repair, and content-addressed proof.

Comment

Inspiration

Concurrency failures are difficult to trust because a bug can vanish as soon as someone tries to reproduce it. Logs show what happened once, tests often prove only a hand-written schedule, and an AI-generated patch can look convincing without proving that it fixes the same failure.

ProofReplay starts from a narrower question: can a human-approved invariant become an inspectable chain from live model-authored counterexample to exact replay to test-first repair?

What it does

The Build Week case is Last Ticket: two independent buyers race for one remaining ticket across an asynchronous payment boundary. The approved rule is simple: confirmed orders must never exceed seeded inventory, and inventory must never become negative.

ProofReplay:

  1. gives a bounded, read-only view of a user-owned toy service to GPT-5.6;
  2. records the model's competing hypotheses, falsifiers, and selected schedule;
  3. executes that schedule through independent HTTP sessions;
  4. minimizes and replays the failure deterministically;
  5. opens a fresh model context for diagnosis and a regression-first repair;
  6. proves that the identical regression bytes fail before the patch and pass afterward; and
  7. seals every handoff in a content-addressed evidence bundle.

The judge-facing flight recorder keeps observed, inferred, verified, and unresolved claims visually separate. It shows both actors, the payment seam, authoritative state, before/after outcomes, repair diff, checks, tool history, model configuration, and provenance.

Verified result

The live GPT-5.6 discovery produced two confirmations from one seeded ticket. Barrier-free evaluation reproduced the violation 20/20 times, and exact replay reproduced it 10/10 times with one semantic signature.

In a separate fresh context, GPT-5.6 wrote the regression first and then a focused atomic quantity-guarded inventory claim. The same regression changed from expected failure to pass; the application tests, TypeScript checks, and full workspace suite also passed. The final live hero chain verifies 21/21 source artifacts.

How I built it

ProofReplay is a TypeScript and Node.js monorepo using Fastify, SQLite via better-sqlite3, Zod contracts, Vitest, pnpm, the OpenAI Responses API, and explicit GPT-5.6 model/reasoning configuration. A bounded coordinator owns execution budgets, tool ordering, scenario reduction, exact replay, fresh-worktree patching, verification, leak scanning, and canonical SHA-256 manifests.

The evidence product is a dependency-free browser UI generated purely from the sealed bundle. Playwright drives the reproducible demo tour, while FFmpeg verifies and encodes the final H.264/AAC submission master.

Codex task ID 019f5d57-a6dc-7912-b597-aa1eb5ae5ad7 contains the majority of the implementation work. The human owner selected the product, invariant, scope, claim boundaries, and external-account actions.

Challenges

The hardest part was evidence discipline. Fixture runs had to remain visibly distinct from live model authorship. Replay-only synchronization could not be presented as discovery behavior. Failed API requests had to become explicit key-free error records instead of quiet passes. Content-addressed bundles had to reproduce byte-for-byte, and model-visible inputs needed leak scans before every live call.

An additional automated safety check declined the first live discovery request before model output. The project preserved that failure honestly, narrowed the framing to local correctness verification without changing the task or permissions, and based every live claim only on the successful disclosed retry and separate repair run.

What I learned

The strongest AI-development demos do not merely show a model producing code. They make authorship, execution, causal interpretation, verification, and unresolved risk independently inspectable.

ProofReplay intentionally does not claim universal correctness. A losing checkout may already hold a payment authorization without a compensation path; other schedules and the separate exactly-once invariant remain outside this proof boundary. Showing that limitation made the result more credible, not less.

What's next

Next steps are additional verified proof families, payment compensation, crash-consistent inventory/order transactions, and adapters for more repositories—while retaining the same human-approved invariant and content-addressed evidence contract.

Built With

Share this project:

Updates