Yichus / Reference

API MCP tools

Every tool in Yichus/Mcp::catalog. Parameters and recorded examples help you choose a tool; the getting-started walkthrough teaches the loop.

• api_guide — Return the pre-written agent guide for building a Bosatsu API with checked access rules. Call this first. Deterministic documentation; no model-generated advice. With no arguments it returns every section; with section it returns the sections whose title contains that text (case-insensitive) and, on no match, the list of titles.
• api_scaffold — Generate a Yichus-first Bosatsu API module: structs, Yichus/Access rules, owner-scoped or public handlers, and a Yichus/Service routing table, plus a matching Yichus/Frontend::FrontendSpec (frontendSource) for api_frontend. The result compiles and verifies; edit it, then api_verify.
• api_add_rule — Return a one-line Yichus/Access AccessRule snippet to paste into an existing AccessSpec list.
• api_verify — Rerun the available safety checks from the typed IR of the given Bosatsu sources. Reports which properties still hold after edits. Topology is an input: undeclared defaults to multi-instance, where RMW and interleaving findings are violations. Do not deploy unless proven is true.
• api_deploy — If api_verify is proven under the declared topology, generate the Yichus API engine JavaScript (handlers + Principal injection + DB IO). Refuses when any property is violated or blocked, and when a property named in require is not proven. The emitted HTTP server refuses to listen unless YICHUS_AUTH is jwt (JWKS), clerk-api-key (API keys checked with Clerk via CLERK_SECRET_KEY), proxy-header (X-User-Id plus YICHUS_TRUST_PROXY_AUTH=1), or dev (YICHUS_DEV_AUTH=1). The engine also serves its routes as MCP tools at /mcp, so an agent can call the deployed API.
• api_compile — Parse and type-check Bosatsu API sources in memory (CompileKernel). No filesystem.
• api_audit — Audit IO composition from typed IR: read-then-write, orphaned IO, and writes without reads. These are diagnostics to interpret in context, not an application-wide safety proof. Use api_verify for the composite API gate.
• api_permissions — Compare declared Yichus/Service route permissions to inferred CRUD from handler effects. A missing or mismatched permission is separate from row access and caller authentication: api_access_check checks resource policies; the server engine enforces route identity and roles.
• api_access_check — Check resource policies from typed IR: OwnerScoped keys must derive from the runtime Principal; Guarded operations and row uses must follow supported declared guards; GuardedOrRoles also permits access when every route reaching the operation requires every listed role. An empty guards list is role-only. PublicReadRoleWrite permits reads and queries on any route but requires every listed route role for mutations, including ID allocation. Public imposes no owner-key or guard discipline. Reports holds/violated/inconclusive. Also returns routes, every declared route with discloses: each stored field path (table.field[].field) its response may carry, kind copied, computed, guard (it only decides which reply is sent) or released, via the release for released, precise false for a possible reach. An empty discloses list means the complete walk found no stored field; discloses is null, with disclosesBlocked reasons, when the walk cannot establish it. Guard use does not prove that the guard expresses the intended business rule, and route authority relies on the server enforcing authenticated identities and roles.
• api_integrity_check — Complete typed causal order existence plus bounded per-cell race, stale-read, and declared Yichus/Spec checks. Inspect the returned claims: top-level ok and WebMCP isError describe tool execution, not whether properties hold. Default schema=legacy-2.2 retains verdicts.invariants; opt in to schema=3.0 for spec-verdict claims with typed subject, operation scope, completion and trust gaps. A declared model hold does not prove its implementation, and a sampled hold is inconclusive in 3.0. Truncated cells without a counterexample remain inconclusive; causal consistency alone does not certify model quality or database executions. TLC is not run; both schema views carry only a diagnostic sketch. For legacy-2.2, view=compact replaces only the inline sketch. For 3.0, it also deduplicates operations into an operationCatalog and uses numeric references in scopes and causal pairs. Both compact views carry a sketch hash and full-view retrieval request; view and schema are independent selectors.
• api_dist_check — Run DistEngine on a declared Yichus/Dist DistSpec (multi-instance schedules, lost updates).
• api_escrow_check — Run AdmissionSolver on a declared EscrowSpec (a State cell) or TableEscrowSpec (a table: one integer per row key, bounds read off another table's row). Pass batch JSON to admit/defer operations; a table spec is admitted against rows. Replay checks the admitted operations only. It does not establish that the handler rejects operations the declaration deferred, so it is not a general proof that the handler enforces the bounds.
• api_report — Build the program-report-2.0 map from the typed IR for whatever style of program the sources are (CRUD, flow, dist, escrow, unrouted IO). overview.surfaces names the present IR surfaces; needed names missing declarations with snippets. Pass format html for a self-contained HTML document.
• api_frontend — If api_verify is proven, generate a self-contained HTML frontend from a Yichus/Frontend::FrontendSpec in the sources. Refuses unknown routes, unrepresentable handler extras, and unproven APIs. Transport (in-process or http) and auth (dev, clerk, auth0, api-key, bearer) are tool args.
• api_add_artifact — Return a paste-ready Bosatsu snippet for a report artifact (AccessSpec, ServiceDef, DistSpec, EscrowSpec, FlowSpec, Spec, FrontendSpec). Pass kind. Pass the same sources as api_report to fill names from the IR, or omit sources for a generic template. If the kind does not apply to those sources, the tool says so instead of emitting a misleading snippet.
• api_law_check — Check declared Yichus/Law obligations. Mode sampled (default) uses seeded generation: holds is bounded observation, never proof. Mode exhaustive checks every value of an accepted finite type or every distinct value of a Bosatsu FiniteObligation list; holds-exhaustive applies only to that recorded scope. Unsupported domains, exceeded limits, unfinished witnesses, and worker failures never become a pass. Violated and inconclusive both mean not done.
• api_lean_check — Ask a configured host (native, Node Wasm, or the isolated browser Lean Wasm page) to compile exact Bosatsu sources and run pinned Lean on supported Yichus/Law obligations. Pass sources to check, or receipt_sha256 alone to fetch the exact full receipt cached by this host. The compact view is the default agent result; view full returns the complete validated run. Its fullReceiptSha256 names exact full receipt bytes, not a portable proof: recompile and recheck across builds. The translator requires a direct Law.check and exactly one direct filled Witness. All three hosts support capture-free nonrecursive unary Bool predicates and a narrow structural List[Bool] predicate with self-calls only on the bound tail of a Nil/Cons match. The native host also supports a checked Int/product grammar with exported literal lean_proof and lean_witness scripts and the optional pinned Mathlib bundle. Lean checks generated recursion termination; author proof terms can cite existing Mathlib theorems. Mathlib is unavailable in the Node/browser Wasm runtime. Verified means generated law and witness theorems passed Lean elaboration and axiom audit over the recorded input type. Native receipts also record independent leanchecker replay; Wasm receipts explicitly set independentKernelReplay false. Compare method, scope, and completion before describing the proof. FiniteObligation is not admitted. A compact not-admitted row means this method could not check the law: withhold proof-dependent changes and seek another proof route. A not-verified row means Lean did not establish proof; inspect the full receipt. Unsupported laws, missing tools, timeouts, and empty obligation sets are inconclusive. The isolated browser Lean page supports the Wasm route through WebMCP; the general browser workbench reports unsupported-host guidance. Worked sources: https://yich.us/reference/api-mcp/examples.html#lean-bool and https://yich.us/reference/api-mcp/examples.html#lean-list and https://yich.us/reference/api-mcp/examples.html#lean-mathlib.
• api_protocol_check — Exhaustively explore a protocol-case-1.0 finite domain against compiled transaction handlers. Requests carry instance and delivery identities; serializable transactions are atomic; commit-unknown branches into committed and uncommitted durable states; external dispatch and response are separate transitions. Declare IO[Bool] invariants over immutable before/after views, required reachability witnesses, typed named inputs, times, external results, and budgets. Holds means only the complete declared finite domain; violated includes a sourced schedule; exhausted budgets and unsupported semantics are inconclusive. Adapter conformance, authenticated principals and absence of unlisted writers remain explicit assumptions. Use the same case with yichus protocol --case case.json files.bosatsu. Case schema, selector vocabulary and a runnable example: docs/protocol-verification.md (https://github.com/snoble/yichus/blob/main/docs/protocol-verification.md).
• api_conformance_check — Check declared Yichus/Spec Conformance and WorldConformance bindings by execution: the compiled handler runs in a real seeded world over generated inputs (one table for Conformance; every table, as one of the declared callers, for WorldConformance), and the declared step is compared against the projected world after every operation. Three-valued verdicts (holds is bounded observation, never proof); divergences render through the declaration's own describe and show_input, and name the caller in the world form. Violated and inconclusive both mean not done.
• api_obligations — The guided commit-strategy surface: which strategy your discharged obligations license (serialized commit, per-key independence, single-write commit, lattice single-write, bounded witness search), and — when a faster one is one obligation away — one pre-written sentence saying what would make this faster plus one paste-ready law snippet. Discharge is fail-closed on verdict status: only laws with a holds verdict count, and holds is bounded evidence, never proof. The engine does not check that a named law expresses its obligation or that it applies to the deployed handler — those bindings are your assertions, restated in the verdict's unverifiedAssertions field — and the licensed strategy stays advisory until a later phase verifies them.
• api_abstraction_map — Draw the program's abstraction ladder: every definition placed at its abstraction height (layer 0 = built only from builtins; each layer composes the ones below), with reuse (fan-in), width (direct dependencies), mass (size: node count of the compiled definition), duplication (shape-isomorphic blocks repeated inside a definition, and copy-paste clone pairs across definitions), and layer-skipping edges measured. Every visual quantity is a defined function of the source's dependency graph and the layout is deterministic, so you can inspect reuse and layer crossings. The layout does not score organization or establish that one graph shape is best. On the browser MCP page this tool also renders the map for the user, so sending sources here changes what they see.
• api_organize — Render one organization lens over the module as the text the CLI's `organize` prints: page (how organized the program is, at a glance: layers, blocks, holes), stack (the blocks by layer in the order a reader learns them, with reuse), conventions (how the project writes each recurring shape and where it disagrees with itself), aid (the separate heuristic reading for a weaker reader; clearly labeled as such), layers (the packages in rows by level, the packages each one uses with how many of their definitions, and the direct effect sites and tables in each package's own definitions; `layers` in the result holds the packages with their definitions and levels, and the package and definition edges, all from type-checked references), effects (each declared route as a tree, in source order, of every effect its handler can reach: the calls to it, the IO values handed to a definition as an argument, the typed branch tests around it, and transaction scopes; `effects` in the result holds one row per effect use with its route, table, site, the chain of definitions with the frames around each position, passedTo and under) or writes (the same with only row writes). The effects lens states structure; it does not judge whether a write should sit under a wrapper or a guard. With a view argument over stack or conventions, an authored view (order, foreground, declared groups, captions) renders under the unchanged page or is refused with the reason. The implementations lens returns a structured comparison: all typed user references, signatures, direct primitive effects, access findings, and located compiled repetition. Its nested groups and role meanings are authored, never inferred architecture or permission proof. The page lists; the reader judges.
• api_world_shape — Describe the in-memory world api_why and api_conformance_check run IO handlers in: per table, the row type, whether the row under an id is one record or the whole list, the record's fields, the id rule, the principal's JSON form and the enum form. Facts about the declared types, never about a run; read it before writing rows or inputs.
• api_why — Evaluate ONE binding on concrete typed inputs and report why the output is what it is. Pick the binding from a diagram or report by its Pkg/Name::binding id. Provide inputs as JSON (missing ones are seeded deterministically); the tool returns the typed inputs and output with named rendering, soundFacts (static dataflow: per-parameter influence that holds for EVERY input), and observed (bounded seeded runs: touched bindings, per-parameter and per-field vary-one-fix-rest differentials). soundFacts and observed are disjoint on purpose: an observed-constant result is NOT independence, and every observed sentence says 'bounded observation, not proof'. IO handlers run against a fresh in-memory world (optionally seeded via rows) and report the table rows after the run; handler differentials rebuild the world from the same seeded rows for every variation (a varied principal's roles against fixed rows flips a gated route).
• api_suggest_properties — Propose Yichus/Law obligations from the program's reified facts. Each suggestion is a complete standalone Bosatsu file whose unfillable pieces are named holes; paste it beside your module, or decline it with a Dismissed binding. Runs the default rules plus any RuleSet declared in the sources.
• api_report_brief — Package the report's derived facts (headline, map, guarantees, needed, facts) with constant writing instructions, ready to hand to any LLM that should produce an orientation narrative. The output is fully deterministic: the engine prepares the data and names the task; the prose is the consumer's. Use api_report for the full artifact.
• api_glance — Compare several programs side by side on one scale: vocabulary share, abstraction layers and mass, duplication and clone pairs, declared mutation flows. Every channel shares one scale across the programs, rows are in name order, and the rendering is deterministic ASCII. Each program is compiled separately with builtin shadowing, so a program that declares a Yichus/* package is read as its own version of it. Use api_organize with the map lens for one program in depth; this is the across-programs view. Same job as yichus glance --program name=files.
• api_properties — The per-binding property digest: for every binding the input files declare, the structural facts the explorer and claim checking read. Pure -- a function of the loaded program, with no clock and no randomness -- and restricted to the packages the input files declare, so builtins do not appear. Same job as yichus properties.
• api_yir — Export the canonical YIR (Yichus IR) of a program: the versioned artifact other tooling reads, with its schema version, packages and binding count. Well-formedness is a refusal, not a warning -- an ill-formed export is never returned, because the point of the artifact is that its shape can be trusted. Same job as yichus yir, which writes it to a file; this returns it.
• api_verify_claims — Check an agent's claims about a program against the program's own facts. Each claim gets a three-valued verdict with the evidence that decided it; absence claims are backed by the agenda's enumeration, so "zero cards in scope" carries the examined count as its evidence. A refuted claim is a successful check that found something -- the call stays ok and the refuted field says so. Use this before reporting a finding, not after. Same job as yichus verify-claims, which reads the claims from a file and turns refutals into a nonzero exit code.
• api_dossier — The one-shot trace dossier: every binding with its source location, snippet, inferred type, effect class and dependencies. With a focus binding, the dossier narrows to that binding's transitive dependency closure, focus first and breadth-first after -- one call instead of a walk. A focus that names no binding, or an ambiguous bare name, is an error listing the candidates, never a silent whole-program dossier. Same job as yichus dossier, which writes the file; this returns it.
• api_fact_diff — Diff the fact families between two versions of a program: which agenda cards appeared, vanished or changed, so a review reads the DELTA a change made rather than re-reading the whole program. Optional delta claims are checked against the same report and answered with refuted, exactly as api_verify_claims answers claims about one version. Same job as yichus fact-diff, which reads the two versions from disk and turns refutals into a nonzero exit code.
• api_diff — Structurally diff two versions of a program binding by binding, from the typed IR rather than the text: what changed inside each binding and where. With verdict, returns the PR-diff dossier instead of the raw report. Both versions are Bosatsu sources, not serialized profiles. Same job as yichus diff.
• api_workbook — Orient in a program, inspect binding contracts, or find what a proposed change can affect. Returns the same JSON artifacts as yichus workbook: package mode includes package summaries, a binding catalog and per-binding detail; impact mode follows reverse dependencies from a required binding; dossier mode follows the focus binding's dependencies. Omit binding in package or dossier mode for the whole program. Unknown or ambiguous focus names fail with candidates instead of silently broadening the answer.
• api_explore — Inspect a program's typed structure. Start with overview for effects, dataflow, structural signals and boundaries. Agenda enumerates located facts with coverage counts (page with nextCursor until absent); it also runs pure bindings on seeded inputs and labels those results as bounded observations, not proofs. Use explore to navigate paths, search to find structural matches, connections for immediate edges, trace for dependencies, trace_flow for provenance edges, and path for a route between bindings. Each verb delegates to the same SystemProfileApi engine as yichus explore. Returns response with the explorer's type and payload. Paths accept Pkg/Path/binding or default/Pkg/Path/binding; root is empty. Only the parameters documented for the selected verb are accepted. Daemon process management and user-authored query programs are not included.
• api_flow — Check whether declared mutations follow their FlowSpec factory before shipping a family of similar handlers. report returns extracted named parts and located divergences; failed means a divergence or declaration error (the CLI exits 1). batch replays operations all-or-nothing in memory, never against a live store; admitted=false is a rejected batch, not a tool error. equivalence compares extracted composition with each mutation on seeded inputs: bounded observation, not proof; not-provable stays explicit and only refuted sets failed, as on the CLI. parts refuses any divergent mutation and returns Bosatsu source only after compiling it. Same engine and selection policy as yichus flow: batch and parts require exactly one selected flow; with no flow name any broken declaration fails selection, with a name unrelated broken declarations are returned as warnings.