Yichus

Workbench

Where to do the work

Once you have a program, you need somewhere to edit it, query it, and check it, on your own or with an agent. Each place below runs the same compiled program and the same checks.

Connect your agent once, then any of these can be driven from it. Inspect, edit, and recheck walks one full session; the worked tool invocations show each request.

Choose the check that matches your question

Use the same source set and revision for comparisons. A declaration supplies an expectation; a checker establishes only the property and domain its method covers. A law or model written during review is a proposed requirement. Passing it does not show that it matches the user’s original requirements; preserve those requirements and explain any proposed change.

Property, tool, and scope
QuestionToolWhat the result covers
Does this API satisfy its applicable checks?api_verifyThe composite gate: compilation, policy coverage, access, route permissions/authority, read-modify-write, and integrity. Warnings and topology assumptions remain visible. It does not automatically run every tool below.
Do routes declare the operations they perform?api_permissionsDeclared permissions compared with inferred CRUD effects. This is separate from caller authentication and row access.
Do database operations respect the resource policy?api_access_checkSupported owner-key, guard, and role-authority rules from typed IR, with findings for unresolved or violated rules.
Did I compose IO incorrectly?api_auditDiagnostics such as orphaned IO and read-then-write patterns. Interpret them in the operation’s context; a clean audit is not an application-wide proof.
Is causal order consistent? Can modeled operations race?api_integrity_checkComplete typed causal-graph checking and separately labeled bounded per-cell interleavings. The schedule limit has a hard cap of 8 operations; incomplete exploration without a counterexample stays inconclusive.
Can failures and message ordering break my distributed model?api_dist_checkThe declared world, failure choices, and explored schedules. Run the distributed-systems examples.
Do transaction retries and uncertain commits preserve my invariants?api_protocol_checkExhaustive exploration only within the declared finite case. State/depth/operation cutoffs, unsupported semantics, or missing required witnesses are inconclusive. Runnable case and schema.
Which operations fit within my resource bounds?api_escrow_checkAdmission or deferral for a supplied batch against declared cell/table constraints and starting rows. Replay checks admitted operations; it does not establish that a handler rejects deferred operations. Run the ledger admission demo.
What properties should I test?api_suggest_propertiesSuggested declarations and named holes. A suggestion is not evidence; fill or explicitly decline it, then run the relevant checker.
Does my function satisfy a declared law?api_law_checkSampled mode generates seeded cases and shrinks counterexamples; holds is bounded observation. Exhaustive mode checks an accepted finite type or explicit Bosatsu value list and names that exact scope. Unsupported domains and unfinished checks are inconclusive.
Has Lean checked a supported law?api_lean_checkA configured host recompiles the exact sources and asks pinned Lean to check the generated law and witness theorems over all Bool values or, for the supported structural List[Bool] shape, all finite lists. The receipt records source and toolchain identities. Unsupported translations and browser-only WebMCP return inconclusive guidance; a generated Lean file alone is not proof.
Does the handler follow my model of state changes?api_conformance_checkCompiled handlers executed on generated operations, compared with the declared model after each step. Passing is bounded observation; it does not establish the access policy.
Do my discharged obligations suggest a faster commit strategy?api_obligationsAdvisory strategy selection from named laws with holds verdicts. The law-to-obligation and law-to-handler relationships remain unverified assertions; this does not authorize dropping coordination.
Do related mutations follow the structure I declared?api_flowCompiled structural conformance and supported transformations. Run the flow tutorial. Structural matching is not arbitrary behavioral equivalence.
Does an agent’s report agree with computed program facts?api_verify_claimsSupported claim kinds return supported, refuted, or not-provable. The tool reports refutations in its result; the CLI exits nonzero on them. Inspect not-provable results too. Run the claim-checking example.
Can I inspect a declared system-property verdict?api_integrity_checkReturns native bounded and structural results for Bosatsu Spec declarations. The CLI equivalent is yichus spec; --require-holds makes a named inconclusive result fail. TLC is not run by either surface yet.

Analysis input recipes provide a complete protocol case and implementation view, with the schemas and source files needed to run them.

For a closed function domain, the CLI accepts yichus law --mode exhaustive --maximum 256 --result finite-laws.json <files>. It checks every value of an accepted finite type, or every distinct value in a Bosatsu FiniteObligation list. The separate finite-law-verdict artifact records which scope was checked, including entries for the distinct listed values after validation, and a typed counterexample when one is replayable. Each listed values entry carries a replayable input, or an encoding error. A null values field on a listed scope, or a listed-unresolved scope, cannot justify a change to a named input. An unsupported domain, unfinished witness, exceeded limit, or worker timeout is inconclusive and exits nonzero. The api_law_check tool above accepts the same mode: "exhaustive" and maximum arguments through both MCP and WebMCP. Their workers enforce a hard deadline; a stopped worker yields no passing verdict and a later request starts fresh. On the JVM, use the dedicated yichus law command for exhaustive mode: generic yichus call api_law_check refuses it because that route does not own a killable worker. For CI, gate on the dedicated command's exit code; a catalog tool's ok means the check completed. Check the top-level mode and allHold together, then retain the artifact's method and finite scope with any exhaustive claim. A runnable explicit-domain example shows the Bosatsu declaration and call. api_obligations currently accepts sampled declarations only; finite verdicts do not select a commit strategy.

An exhaustive verdict is a local evaluation by the trusted Yichus engine over the supplied source. The JVM yichus law command snapshots file bytes and checks the worker result against that source identity and verdict shape. npm MCP and browser WebMCP compile their in-memory sources inside killable engine workers. These surfaces do not independently rerun every obligation before returning a verdict. Keep it with that run and rerun after a source or build change; copied JSON alone is not an accepted proof.

For a supported direct Obligation[Bool] or structural Obligation[List[Bool]], run yichus lean --toolchain /private/read-only/lean --source law.bosatsu --json or configure the npm MCP proof host as described in the connection guide. The browser WebMCP cannot launch Lean; api_lean_check there explicitly reports that a proof host is required. A verified receipt covers its recorded input type and named witness theorem. The supported list translator proves its law by induction over all finite Boolean lists. This is a local run result, not a reusable certificate.

api_report assembles the program’s declarations and evidence. api_why explains concrete runs and separately reports static facts. An organization diagram describes structure; it is not a substitute for any of these checks.

Explore a running application

Where this fits

Do it