-
-
The counterexample in focus: $2,399 reviewed, $23,999 changed, $23,999 committed — invariant violated, 9 steps minimized to 3.
-
The landing at the moment the race commits — the only color that ever enters the universe.
-
Explore Futures: 36 schedules, 27 violating futures, the shortest failure ready to focus.
-
Verify: the exact counterexample replayed — BLOCKED, STATE_CHANGED, 0 surviving counterexamples.
-
Ledger: inspect_expense binds a review token to $2,399 · v7 — two live WebMCP tools on the rail.
-
The human edits to $23,999 · v8; the unsafe tool approves it against the v7 review — the recorded race.
Inspiration
Software used to have one operator at a time. WebMCP gives the same live application two: a human using the interface and an AI agent invoking structured tools. Each path can look correct in isolation while their interleaving is unsafe — the agent inspects one version of an object, the human changes it, and the agent then commits an action based on a state that is no longer true. This is not an agent-quality problem: in our recorded race the agent behaves exactly as instructed. It is an application-contract problem, so the repair belongs in the tool contract. Playwright tests your pages; agent evals test your prompts. Nobody was testing the states created when both operators act on the same application at the same time. So we built the testing tool for that.
What it does
Paradox is a testing tool for WebMCP apps. It records semantic operations from a real WebMCP application, explores every valid human-agent interleaving of those operations, evaluates every reached state against business invariants, and returns the shortest replayable counterexample. Then it proves the fix: a constrained semantic version guard on the tool contract, verified by replaying the exact counterexample (blocked with STATE_CHANGED) and re-exploring the complete bounded model.
The recorded race, live on the site (nothing prerecorded or hardcoded):
- The agent calls
inspect_expenseand reviews expense 481 at $2,399, version 7. - The human edits the amount to $23,999, version 8.
- The agent calls
approve_reviewed_expensewith the review token it already holds. - The intentionally unsafe implementation approves $23,999 · v8 against a v7 review.
- Paradox explores all 36 schedules, merges 11 equivalent branches, and finds 27 counterexample futures; the shortest minimizes 9 machine steps to 3 essential operations.
- The version guard is applied to the tool contract; the exact counterexample replays as blocked — STATE_CHANGED; guarded re-exploration reaches 0 surviving counterexamples (36 schedules / 34 states).
WebMCP leverage
Every agent operation runs through real tools registered on document.modelContext (with a navigator.modelContext fallback) — nothing is simulated in the UI. The capability surface is dynamic and state-scoped: 2 tools on the ledger, 3 during exploration, 4 at the finding; stale tools retire through an AbortController, and toolchange keeps the on-page capability rail truthful to the actual registry. Tool results carry guide fields, so the tools themselves steer an agent (or a judge) through record → explore → repair → verify. Spec conformance details we sweated: execute callbacks return plain values (the host serializes), inputs are zod-validated, readOnlyHint annotations are accurate, and a Permissions-Policy: tools=(self) header gates the surface. Verified live end-to-end in the ChatGPT in-app browser — including an improvised amount ($1,337) proving every number is computed, not canned.
How we built it
The engine is deterministic TypeScript — no LLM decides what is safe. Bounded breadth-first exploration over micro-step interleavings, canonical state hashing with equivalent-branch merging (multiplicity preserved), invariant evaluation at terminal states, operation-level counterexample minimization, exact replay, and re-exploration for repair verification. The app is Next.js (App Router) with Zustand; the landing is a physics-true relativistic black hole in WebGPU whose only color enters when the race commits its violation — and drains back out as the guard eliminates every dangerous future.
The SDK ships the complete tester (bun add github:Joe-Simo/paradox-webmcp), including a fully automatic tier: record one line per operation (actor, reads, writes) and analyzeRecording synthesizes the model, explores every interleaving, and reports every stale-belief commit; verifyRecordingRepair proves the guarded fix. A cross-validation test expresses the expense race purely through the public SDK API and reproduces the lab engine's published numbers exactly — two independent implementations agreeing.
Challenges we ran into
Making tool callbacks read live state (not stale React closures); rotating tool surfaces without leaking stale capabilities (AbortController lifecycles with rollback on partial registration failure); keeping every displayed number traceable to engine data; and building an adversarial review loop — 22 review agents across nine dimensions verified every claim against the code, the spec, and the live deployment before submission.
Accomplishments that we're proud of
A real ChatGPT clean-room pass on the production site: the full golden path through live WebMCP tools, surfaces rotating 2 → 3 → 4, the race reproduced and blocked with STATE_CHANGED on a non-scripted amount. Strict TypeScript, 24 unit tests, 5 Playwright e2e (including accessibility), and a 2:00 4K60 demo rendered entirely from the live product.
What we learned
The agent is never the culprit — the tool contract is. The shippable pattern that falls out of Paradox is simple: WebMCP write-tools should carry the version their belief was formed on and reject stale commits with STATE_CHANGED. That one contract change turns an intermittent, unreproducible race report into a deterministic, provable fix.
What's next for Paradox
The expense scenario is a reference implementation of a category, not the category itself: the identical race ships in carts, bookings, refunds, approvals, and permissions the moment an agent and a human share live state. Next: richer automatic hazard classes beyond stale-commit, broader invariant libraries, and CI integration so every WebMCP app can explore its futures before its users do.
Honesty notes
Exploration is bounded and reports incompleteness honestly; zero findings means none survived the explored model — not universal correctness. The demonstrated repair is a constrained semantic version guard, not arbitrary source synthesis.
Try it (2 minutes)
Live: https://www.paradoxwebmcp.com · Docs: https://www.paradoxwebmcp.com/docs · Source: https://github.com/Joe-Simo/paradox-webmcp — testing instructions for a WebMCP-capable browser are in the README.
Built With
- bun
- next.js
- playwright
- react
- tailwindcss
- typescript
- vercel
- webgpu
- webmcp
- zustand
Log in or sign up for Devpost to join the conversation.