Paradox

Make human-agent
time executable.

Open-source semantic instrumentation and bounded correctness testing for stateful WebMCP applications.

01

Install from the public repository

The challenge release is installable directly from GitHub. It exports semantic event, invariant, and state-scoped WebMCP lifecycle primitives.

TerminalTypeScript
bun add github:Joe-Simo/paradox-webmcp
02

Record domain operations, not clicks

Wrap the service boundary shared by the human interface and WebMCP callbacks. Declare actor, source, read set, write set, versions, and canonical state hashes.

semantic-events.tsTypeScript
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 },
});
03

Express the business rule

Invariants are deterministic functions over previous state, the semantic event, and current state. An LLM never decides whether a branch is safe.

invariants.tsTypeScript
import { defineInvariant } from "paradox-webmcp";

export const reviewedStateMatchesCommit = defineInvariant({
  id: "review_version_matches_commit",
  title: "Reviewed state must equal committed state",
  evaluate(previous, event, current) {
    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: "Reviewed state must equal committed state",
          explanation: `Reviewed v${reviewed}; committed v${committed}.`,
          relevantEventIds: [event.id],
        };
  },
});
04

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.

webmcp-surface.tsTypeScript
import { activateToolSurface } from "paradox-webmcp";

const stop = activateToolSurface({
  context: document.modelContext,
  tools: [inspectExpense, approveReviewedExpense],
  onToolsChanged: (tools) => renderCapabilityRail(tools),
  onError: (error) => reportRegistrationFailure(error),
});

// Remove every tool as soon as this page state becomes invalid.
return stop;
Client requirement

WebMCP tools exist while the page is open in a browser that exposes document.modelContext. Elsewhere, Paradox labels local evaluation controls instead of claiming tools are registered.

05

Know the explored boundary

  • Paradox currently analyzes instrumented deterministic domain models.
  • 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.

See the instrumentation operate a real WebMCP race.

Run the lab