Make human-agent
time executable.
Open-source semantic instrumentation and bounded correctness testing for stateful WebMCP applications.
Install from the public repository
The current release is installable directly from GitHub. One package exports the complete tester: automatic race analysis from recorded operations, the bounded interleaving explorer, deterministic invariants, semantic events, and state-scoped WebMCP registration.
bun add github:Joe-Simo/paradox-webmcpAnalyze your app automatically
Declare what each operation read and wrote — one line each — and analyzeRecording does the rest: it synthesizes the model from the recording, walks every interleaving, and reports every schedule where an operation committed on an overwritten belief, minimized to the essential operations. verifyRecordingRepair proves the version-guarded fix. No hand-written model, no hand-written invariant. Every recorded flow becomes a concurrency test tailored to your app.
import { analyzeRecording, createRecorder, verifyRecordingRepair } from "paradox-webmcp";
// 1. Record: one line per operation — what it read, what it wrote.
const recorder = createRecorder();
recorder.record("inspect_expense", { actor: "agent", reads: ["expense:481:version"], writes: ["review:481"] });
recorder.record("edit_expense_amount", { actor: "human", reads: [], writes: ["expense:481:version"] });
recorder.record("approve_reviewed_expense", { actor: "agent", reads: ["review:481", "expense:481:version"], writes: ["expense:481:status"] });
// 2. Analyze: every interleaving, automatically. No model, no invariant.
const analysis = analyzeRecording(recorder.events());
analysis.hazard; // → approve committed after its reads were overwritten
// 3. Repair and prove: version-guard the writers, replay, re-explore.
const verdict = verifyRecordingRepair(recorder.events(), analysis.exploration.counterexample!.trace, {
guarded: ["inspect_expense", "approve_reviewed_expense"],
});
// verdict.verified → the hazard is gone in every ordering.Register only the tools valid now
The lifecycle helper registers one state-specific tool surface, listens for registry changes, and removes stale capabilities with an AbortController.
import { activateToolSurface } from "paradox-webmcp";
export function exposeLedgerTools() {
const context = document.modelContext ?? navigator.modelContext;
if (!context) return; // no WebMCP host on this page
const stop = activateToolSurface({
context,
tools: [inspectExpense, approveReviewedExpense],
onToolsChanged: (tools) => renderCapabilityRail(tools),
onError: (error) => reportRegistrationFailure(error),
});
// Call stop() as soon as this page state becomes invalid.
return stop;
}WebMCP tools exist while the page is open in a browser that exposes document.modelContext (or navigator.modelContext). Elsewhere, Paradox labels local evaluation controls instead of claiming tools are registered.
To connect a real host: in Chrome 149+, enable chrome://flags/#enable-webmcp-testing and inspect registrations in DevTools → Application → WebMCP (or drive the tools with a client such as the Model Context Tool Inspector extension). The ChatGPT desktop app's in-app browser connects on its own when it opens a page that registers tools.
Record full-fidelity semantic events
For the complete audit trail the lab itself keeps — actor, invocation source, versions, and canonical state hashes on every operation — wrap the service boundary shared by the human interface and WebMCP callbacks with createSemanticEvent.
import { createSemanticEvent } from "paradox-webmcp";
const event = createSemanticEvent({
id: "evt_003",
actor: "agent",
action: "approve_reviewed_expense",
invocationSource: "webmcp",
entityIds: ["expense:481"],
reads: ["expense:481:version", "review:v7"],
writes: ["expense:481:status"],
preStateHash,
postStateHash,
logicalTime: 3,
metadata: { reviewedVersion: 7, committedVersion: 8 },
});Prove exact business rules
Beyond the structural stale-commit race, express precise rules as deterministic functions and run them with the modeled exploreInterleavings / verifyRepair tier — the expense race expressed that way reproduces the lab engine's published numbers exactly. An LLM never decides whether a branch is safe.
import { defineInvariant } from "paradox-webmcp";
type Ledger = { expenses: Record<string, { version: number }> };
type ReviewEvent = { id: string; entityIds: string[]; metadata: { reviewedVersion: number } };
export const reviewedStateMatchesCommit = defineInvariant({
id: "review_version_matches_commit",
title: "Approved state must equal inspected state",
evaluate(previous: Ledger, event: ReviewEvent, current: Ledger) {
const reviewed = event.metadata.reviewedVersion;
const committed = current.expenses[event.entityIds[0]].version;
return reviewed === committed
? { ok: true }
: {
ok: false,
invariantId: "review_version_matches_commit",
title: "Approved state must equal inspected state",
explanation: `Reviewed v${reviewed}; committed v${committed}.`,
relevantEventIds: [event.id],
};
},
});Know the explored boundary
- Automatic analysis needs only each operation's declared reads and writes; exact semantic invariants need a small hand-written model.
- Modeled state must be JSON-plain data — plain objects, arrays, strings, numbers, booleans, null. Map, Set, and Date are rejected loudly rather than hashed unsoundly.
- Exploration is bounded and reports an incomplete result if that bound is reached.
- The included product contains one complete expense-approval scenario.
- The demonstrated repair is a semantic version guard, not arbitrary source synthesis.
- Zero findings means none survived the explored model — not universal correctness.