Guide

Connect an agent to the WebMCP workbench

For a first project, use the QuickStart for Cursor, Codex, Claude Code, and OpenCode: connect the browser, build a calculator with generated Why explanations, and save a local copy.

Use the browser connection to watch the agent’s map, evaluations, and app in an open tab. Use the Node server when you want the tools through a local process. Both use the same checked Yichus/Mcp::catalog.

The main browser workbench runs the pure engine. For browser proof checks, open the dedicated isolated Lean Wasm page. It exposes api_lean_check through WebMCP, compiles the supplied Bosatsu source in the shared engine, and runs pinned Lean in a browser worker. Its source-bound local receipt records that independent native leanchecker replay was not run.

Local Lean proof hosts

Install Java 17, build the JVM Yichus fat JAR, and install the pinned Lean toolchain in a private, read-only location. Start the npm API MCP server with both --proof-host /absolute/path/to/yichus.jar and --lean-toolchain /absolute/path/to/lean. The host checks exact source bytes in a supervised worker and returns a compact, source-bound local-run view by default. Pass its fullReceiptSha256 back as receipt_sha256 to the same server to fetch the exact full receipt; compact rows distinguish a law the translator did not admit from a generated proof that was not verified. Neither is a proof or a counterexample. the server retains a bounded in-memory cache, so a cache miss requires a fresh check. The full receipt carries diagnostic reasons omitted from the compact view. The digest names this host's exact output bytes, so use it with the host that produced it. This method covers direct Bool laws and the documented structural List[Bool] law and witness; unsupported laws and FiniteObligation remain inconclusive.

Set JAVA_HOME to the absolute Java 17 installation when the proof host is a JAR. The server runs that installation's bin/java instead of resolving a java command through PATH.

node /absolute/path/to/yichus/packages/yichus-api-mcp/dist/cli.js \
  --proof-host /absolute/path/to/yichus.jar \
  --lean-toolchain /private/read-only/lean

For a Node-only host, install the pinned slim Lean WebAssembly release in a new private directory and select it instead of the JVM host:

yichus-lean-wasm-install --output /absolute/private/lean-wasm
yichus-api-mcp --lean-wasm-root /absolute/private/lean-wasm

Node runs the same supported Bool and structural list translations. Its receipt is a distinct lean-wasm-law-run: Lean accepted the generated theorems and the axiom audit, while independentKernelReplay is false. The native route separately replays with leanchecker. Read the method and completion fields before describing either result. The Node command-line equivalent is yichus lean FILE --lean-wasm-root DIRECTORY.

The npm package alone does not include a JVM proof host or Lean. The configured host and toolchain are trusted local inputs. The checker hashes the toolchain before and after each run, but a concurrent writer to its directory can defeat that check; keep that installation private and immutable while proving. A receipt must be rechecked against current sources for a later build.

Native browser site tools

For Lean proofs, open the Lean Wasm page directly and wait for its ready status. Its isolated worker requires shared memory and may reload once. The runtime is downloaded on the first proof. The regular workbench below continues to offer the other catalog tools. When building the site from a checkout, install the pinned Wasm runtime and set YICHUS_LEAN_WASM_ROOT to that directory for scripts/build_web_deploy.sh; the site artifact check refuses a published Lean page without its pinned runtime.

In Codex’s built-in browser, open api-mcp.html as the top-level page and wait for the catalog-ready status. Select Site tools in the address bar, then Available site tools, and ask the agent to call api_guide. No MCP server configuration or ?webmcp=1 is needed for this route. Keep the tab open.

Yichus registers on document.modelContext when supported, otherwise navigator.modelContext. When both are present, the document registry takes precedence over the navigator polyfill. Codex currently discovers tools only in the top-level document: a hosting viewer that embeds this page in an iframe hides its tools. Serve the page directly, including from localhost during development. See the official site-tools documentation for availability and browser permissions.

For private pages hosted on Valet, add __valet_webmcp=1 to the normal artifact URL. Valet's direct mode places the artifact at the top level on its isolated content origin while retaining authentication. This is distinct from Yichus's webmcp=1 relay flag below. See Valet's WebMCP guide.

Browser: the local relay

To call api_lean_check through the relay, open the Lean Wasm page with WebMCP enabled and discover its registered source. The steps below use the main workbench for the other tools.

1. Configure a compatible WebMCP host or the @yichus/mcp local relay in your MCP client.
2. Open the workbench with WebMCP enabled and wait for its ready status.
3. Through the local relay, call webmcp_list_sources, then webmcp_list_tools. Match each tool’s sources to this tab and call its returned public name (which may have a tab suffix). It is registered as yichus-api-mcp.
4. Call api_guide through the discovered tool. A returned guide confirms that the engine and connection both work.

An ordinary browser tab cannot receive MCP calls by itself. It needs a host that supports native site tools or the relay. Keep the tab open while the agent works.

pnpm install
pnpm run yichus-mcp:build

{
  "mcpServers": {
    "yichus-browser": {
      "command": "node",
      "args": ["/absolute/path/to/yichus/packages/yichus-mcp/dist/cli.js"]
    }
  }
}

If the tab is missing: confirm ?webmcp=1 is in its URL, leave it open, and reconnect the client to the relay. If the engine fails to load: reload the page before retrying discovery.

What changes on the page

• api_abstraction_map draws the supplied program’s dependency map.
• api_why fills the evaluator with its inputs, output, and evidence.
• api_organize returns a text lens; lens: "stack" also draws the engine’s stack picture.
• yichus_app_open runs a generated app that you can also use.

For a ready-made starting point, use a tool request from the before-and-after examples. Each request includes its complete source. The request’s sources field is an array of file objects. Use the types in the tool schema for its other parameters.

Node: a local MCP server

Build @yichus/api-mcp from a checkout; it is not published to npm. You need Node 20+, pnpm, and the Scala toolchain available through Nix:

git clone https://github.com/snoble/yichus
cd yichus
pnpm install
nix-shell --run 'sbt -J-Xmx4G --no-server "mcpjs/fastLinkJS"'
pnpm run yichus-api-mcp:build
node packages/yichus-api-mcp/dist/cli.js --help

Put this entry in your MCP client’s configuration, with your checkout’s absolute path:

{
  "mcpServers": {
    "yichus-api": {
      "command": "node",
      "args": ["/absolute/path/to/yichus/packages/yichus-api-mcp/dist/cli.js"]
    }
  }
}

Restart the client, list its tools, and call api_guide. If the process exits, run the configured command in a terminal and resolve its startup error. Check the Node version and absolute path.

Where the source goes

The browser performs analysis in the tab and gives the checker no filesystem access. Source arguments and results pass through the relay to your MCP client and agent; Yichus does not upload them to a hosted checker. The Node route sends the same data between the client and local process over stdio.

Follow the inspect–edit–recheck workflow · Tool catalog