@yichus/api-mcp

MCP server that guides an agent to write a Bosatsu API the Yichus engine can prove safe, then deploy as JavaScript.

This package is a JSON-RPC transport. The MCP itself is a Yichus engine with Bosatsu configuration:

• Yichus/Mcp declares the tool catalog and the agent guide.
• Yichus/Access is the canonical authoring layer for Principal, Policy, AccessRule, and AccessSpec.
• Yichus/Data and Yichus/Service stay Yichus-owned (effect meaning and analysis-visible route markers).
• ApiMcp / ApiSafety / ApiScaffold are deterministic Scala. There is no model-generated advice in the loop.

User stories

1. A non-expert asks a cheap LLM for an API. The agent calls api_guide, then api_scaffold, edits the Bosatsu, and api_verify after every change. It cannot honestly say the API is safe unless the verdict is proven.
2. The agent edits generated code. Rails-like templates are a starting point. After a leaky db_read(..., "other-user"), verify reports access:notes violated and leaves compiling / coverage proven. Safety is re-proven from the IR, not assumed from the template.
3. The user deploys. api_deploy refuses unless every property is proven under the declared topology, then emits a Node engine that injects Principal and interprets Yichus/Data IO (pure / flat_map). HTTP listening is a refuse-by-default trichotomy: YICHUS_AUTH=jwt verifies Authorization: Bearer against a JWKS; YICHUS_AUTH=clerk-api-key checks each Authorization: Bearer API key with Clerk (CLERK_SECRET_KEY) and acts as the key's user or organization, for scripts and servers; YICHUS_AUTH=proxy-header plus YICHUS_TRUST_PROXY_AUTH=1 is the X-User-Id path; YICHUS_AUTH=dev plus YICHUS_DEV_AUTH=1 is a demo user-switcher. Unset or unknown modes refuse to listen. yichusApiEngine.handle stays available in-process. Handler code never constructs Principal. Do not wrap db_* in thunks; they already return IO. api_frontend generates screens over the same proven routes (in-process or HTTP; Dev / Clerk / Auth0 adapters).
4. Topology is a declared input. Owner-scoped keys are the caller’s user_id. Read-modify-write handlers are violated under the default (multi-instance) topology; pass instances: 1 for a genuinely single-instance deploy to accept them as warnings, or run them in a transaction (or a single writer) when more than one engine instance is live.

Install and connect

The npm release is being prepared; use a checkout until publication. Build the shared compiler and the package:

pnpm install --frozen-lockfile
nix-shell --run 'sbt -J-Xmx4G --no-server mcpjs/fastLinkJS'
pnpm run yichus-api-mcp:build

Package builds normally vendor the fresh mcpjs/fastLinkJS output. To use an already built engine, set YICHUS_APIMCP_BUNDLE to its absolute path when running the package build. CI uses the exact engine staged for the website in either link mode. An explicit missing bundle fails the build and removes any previous vendored engine; it never falls back to another link mode.

Configure your MCP client with an absolute path:

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

The release tarball includes the Scala.js compiler. After publication, Node 20+ is enough and the server can be started with npx -y @yichus/[email protected]. It needs no Java, Nix, checkout, or browser. Tool requests compile and analyze the supplied sources locally. The optional api_lean_check tool has two local backends. The native backend needs Java 17, a separate trusted JVM Yichus CLI, and the pinned Lean installation. Start this server with both --proof-host /absolute/path/to/yichus.jar and --lean-toolchain /private/read-only/lean. For a Node-only Wasm backend, install the pinned public slim runtime once, then pass its absolute root:

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

The installer downloads and verifies a 290 MB release archive, then installs the 67 MB Wasm binary and its 81 MB Lean library. It refuses to replace an existing runtime. Node 20+ runs this WebAssembly build; Java is unnecessary on that route. Select one backend per server. Without one, the tool reports unsupported-host guidance. The isolated browser Lean page provides the Wasm route through WebMCP; the general browser workbench reports unsupported-host guidance. Point JAVA_HOME at an absolute Java 17 installation when --proof-host is a JAR; the host does not resolve java through PATH. Keep the toolchain private and read-only while a proof runs. Its hashes are checked before and after execution, but a concurrent writer can defeat that check. The Wasm receipt records Lean kernel elaboration and an axiom audit, and says independentKernelReplay: false: it does not claim the separate native leanchecker replay. It pins the Wasm, glue, and library hashes, and still depends on trusting the local runtime installation during the check. Current Lean translation covers direct Obligation[Bool] laws and the documented structural Obligation[List[Bool]] law and witness. The list translator permits only a self-call on the bound tail of a Nil/Cons match; other recursive shapes are inconclusive. On the native host, Int and declared products of Int fields also have an assisted proof path: export literal lean_proof and lean_witness scripts and install the optional pinned Mathlib library with node scripts/install_lean_mathlib.mjs /path/to/lean-4.34.0-platform from the repository. The generator translates the actual selected predicates and helpers; Lean checks termination and both the universal law and existential witness. Scripts may cite existing theorems such as ZMod.pow_card_sub_one_eq_one. See the worked modular inverse. The CLI's --emit-lean Proof.lean saves the generated module before verification so authors can inspect definitions and goals; source output alone is not evidence. Mathlib is a separate, large native library; the Node and browser Wasm routes do not load it. The default response is a compact view with every obligation's status, exact source identity, and a fullReceiptSha256 digest. Call api_lean_check again with only receipt_sha256 to fetch the exact full receipt from this live server; the bounded cache can evict it, in which case rerun the source check. Pass view: "full" with sources to receive the complete receipt immediately. The digest identifies this server's exact JSON output bytes, including its final newline; a separate CLI --result file has its own byte digest. Use the digest with the server that produced it. The full receipt carries diagnostic reasons omitted from the compact view. The receipt is bound to the supplied source bytes and is a local-run result, not an importable proof certificate. The stdio transport runs the engine in a child process with a 120-second request deadline. A timeout, cancellation (notifications/cancelled), or worker crash returns a JSON-RPC error; the next request starts a fresh engine. Input lines and worker responses are capped at 16 MiB. A transport error is never evidence that a property holds.

Call api_guide first, then discover the current catalog with tools/list. This is the browser API workbench's core catalog; live browser editors, visible feedback, and yichus_app_* sessions are provided separately by @yichus/mcp, the browser relay.

For terminal use and CI, yichus shares this packaged engine:

yichus tools
yichus verify notes-api.bosatsu --instances 1 --output verdict.json
yichus call api_abstraction_map --source notes-api.bosatsu --output map.json

verify fails unless verdict.proven is exactly true. Other catalog checks are available through call and explicit --expect assertions. See release preparation for packed-artifact validation and publication ordering. Nothing is published by building.

Tools (from Yichus/Mcp::catalog)

| Tool | Kind | |------|------| | api_guide | Pre-written workflow and access rules | | api_scaffold | Generate a Yichus-first Bosatsu module | | api_add_rule | AccessRule("table", OwnerScoped) snippet | | api_compile | In-memory parse + typecheck (CompileKernel) | | api_audit | IO composition findings | | api_permissions | Declared vs inferred route permissions | | api_access_check | Per-user access proof (holds / violated / inconclusive) | | api_integrity_check | Complete typed causal consistency plus bounded races, stale reads and declared models; optional view: "compact" retains all decisions with a retrievable witness hash | | api_dist_check | DistEngine multi-instance schedules | | api_escrow_check | AdmissionSolver bounded-balance check | | api_verify | Composite api-safety-1.0 verdict | | api_deploy | JS engine, gated on proven; HTTP listen requires YICHUS_AUTH | | api_report | program-report-2.0 program map (CRUD, flow, dist, escrow, unrouted IO) | | api_frontend | Verified HTML app from Yichus/Frontend::FrontendSpec | | api_add_artifact | Paste-ready snippet for a missing report declaration |