Tutorial

Your first WebMCP session

The WebMCP workbench lets an agent call Yichus tools in your browser while you inspect the same program. The abstraction map shows its dependencies; the evaluator lets you try inputs; the app panel runs a generated interface.

Start with the before-and-after examples. They show a copied stock rule becoming a shared definition and a Notes handler whose access violation disappears when its row key is fixed.

1. Connect and load the source

Connect your agent, keep the workbench open, and wait for its ready status. Call api_guide, then api_compile with all files in the program. Fix any compile error before interpreting a check. If the tools are missing, use the connection guide’s discovery check.

Set sources to an array of {fileName, source} objects, where source contains the complete UTF-8 file. The examples include ready-to-use requests with that source already filled in.

2. Choose a question, then a lens

The stack lens also draws the engine’s SVG in the workbench. page gives an organization overview. aid returns explicitly labeled heuristics. The lens reference explains their fields and limits.

3. Find the change worth making

Ask the agent to name the definition and evidence behind its diagnosis. A clone finding can motivate a shared helper; a failed owner-key check names an operation to repair. A diagram’s shape alone is not a correctness verdict.

Show me the program’s dependencies and repeated bodies. Explain one concrete maintenance problem, then make a focused refactor. Run the same lens afterward and check that the behavior we rely on still holds.

When an agent calls api_abstraction_map, its source set drives the displayed map. To evaluate one of those definitions, call api_why with the same sources and its full Package/Name::binding ID.

4. Re-run the same checks

The check chooser maps each question to its checker and distinguishes static and bounded evidence. Check who may do what has editable ownership and role-boundary examples.

For a declared state-machine property, call api_integrity_check with schema: "3.0" and read each claim’s method, scope and completion. The evidence guide explains the native result and its TLC and Lean limits.

For a supported Bool, structural List[Bool], or Int/product law, api_lean_check uses the pinned Lean checker on an explicitly configured host. Native hosts support all three admitted grammars; Node Wasm and the isolated browser Lean page support Bool and structural list laws. Int/product proofs require the native Mathlib bundle. The general browser workbench reports unsupported-host guidance for this tool. Use the proof-host setup for local MCP or yichus lean from the CLI. Its compact result names each checked predicate and the exact source, with a digest for retrieving the full source-bound receipt. Keep that receipt with any proof claim. The modular-inverse example translates a Bosatsu implementation and uses an existing Mathlib theorem in its proof.

Compile the edited files, repeat the lens call, and compare the result. For a refactor, also test the relevant outputs. For a defect, rerun the failing check and its counterexample. The worked examples provide both versions, raw evidence, and recorded executions.

Run api_verify for a composite verdict. proven means no applicable property is violated or blocked under the stated assumptions; warnings can remain. inconclusive means a specialized check did not settle the question. Keep the source set and topology fixed when comparing results. The full Notes example explains the topology choice. A blocked property was not established because its check could not run or finish. Warnings can include bounded evidence or deployment assumptions; the composite flag is not an unconditional proof of the application.

5. Run the app

api_frontend checks a FrontendSpec—a declaration selecting existing routes as views—and generates an interface after verification succeeds. In the browser, yichus_app_open exposes a page-specific wrapper to run it in the app panel. Inspect that tool’s schema: its sources parameter currently takes a JSON-encoded string, unlike the catalog’s native array. If generation refuses, fix the named guarantee or route-shape problem.

Starting a new API? api_scaffold creates API and frontend sources; compile both returned files before editing them. Worked tool invocations cover the full Notes app and ProjectHub. The tool catalog lists every parameter.