Reference

CLI reference

Get the CLI

The yichus binary is built from source. You need git, a JVM (17+), and sbt; sbt assembly writes yichus.jar under target/:

git clone https://github.com/snoble/yichus && cd yichus
sbt assembly
alias yichus="java -jar $(pwd)/target/scala-*/yichus.jar"

Build the two MCP servers

Two npm packages wrap parts of the same engine. @yichus/api-mcp serves the API Safety MCP tools (scaffold, verify, report — the surface documented under API MCP docs). @yichus/mcp is the local relay that opens the hosted calculators and playground with WebMCP enabled.

Neither package is published to npm, so npx will not find them. Both build from the checkout above, and neither needs the jar:

pnpm install
pnpm run yichus-api-mcp:build
node packages/yichus-api-mcp/dist/cli.js

pnpm run yichus-mcp:build
node packages/yichus-mcp/dist/cli.js

Neither replaces the CLI. The commands below, such as explore, dist, and fact-diff, need the jar.

Commands

Commands on the yichus binary. Each page includes the current usage, options, and available subcommands.

• yichus build — Type-check Bosatsu files with Yichus packages
• yichus eval — Evaluate a binding and print result
• yichus sim — Generate interactive HTML simulation
• yichus simapp — Generate simulation app from .sim.bosatsu config
• yichus deploy — Execute the declarative deploy manifest
• yichus matchless — Export Matchless IR and metadata sidecar
• yichus spec — Run native bounded and structural checks of declared Bosatsu properties (TLC is not yet available)
• yichus tla — Retired TLA+ sketch command; use spec for native checks
• yichus admit — Solve batch admission against declared escrow invariants
• yichus law — Check declared Yichus/Law obligations by seeded generation, or propose properties with --suggest
• yichus lean — Prove supported Bool laws on a configured host with the pinned Lean toolchain
• yichus conformance — Check declared Yichus/Spec Conformance bindings against the compiled handlers by execution
• yichus dist — Check declared distributed-world specs by deterministic simulation
• yichus protocol — Explore declared finite transaction protocols with atomic states, faults, and sourced counterexamples
• yichus flow — Verified mutation flows: conformance, parts, batch, equivalence
• yichus yir — Export canonical YIR (validated on emit)
• yichus dossier — Export a one-shot trace dossier over the provenance graph
• yichus workbook — Export package/impact workbook artifacts for agents
• yichus verify — Enumerate interleavings for IO-heavy source
• yichus audit — Audit IO patterns in Bosatsu files
• yichus service — Service and CRUD scaffolding commands
• yichus api — Scaffold, verify, and deploy a Yichus-first Bosatsu API
• yichus access — Prove per-user data access from Matchless IR
• yichus explore — Emit system profile JSON
• yichus properties — Emit a canonical per-binding property digest
• yichus verify-claims — Check an agent's report against computed program facts; inspect supported, refuted, and not-provable results
• yichus why — Evaluate one binding on typed inputs and report why the output is what it is
• yichus glance — Compare N programs' glance channels on one shared declared axis
• yichus organize — Render the organization lenses (page, vocabulary, stack, conventions, map, flow, diff) over Bosatsu files
• yichus diff — Diff two explorer profiles structurally
• yichus fact-diff — Diff the fact families between two program versions
• yichus serve — Start explorer HTTP service
• yichus mcp — Start explorer MCP server
• yichus playground — Start browser-based simulation editor
• yichus daemon — Explorer daemon
• yichus bosatsu — Passthrough to bosatsu CLI