Guide

Read a Bosatsu Spec verdict

Declare a property in Bosatsu with Yichus/Spec, then ask Yichus what its native checker established. The checker decides whether the complete typed causal graph admits an order and separately explores bounded operation schedules for each state cell. A property of the declared model does not by itself prove that an implementation follows that model.

Use the same evidence in each interface

The CLI checks a program with a declared Property or StepProperty:

yichus spec --schema 3.0 --view compact --max-ops 8 --output verdict.json model.bosatsu handlers.bosatsu

For an input-indexed handler, declare transition2("move_till", move_till, step, show_input) inside the Bosatsu StateModel. The literal name must match the referenced handler binding. Put these calls in a literal op_transitions list in the Spec binding; a helper-built list is rejected because it can substitute a different transition value. Yichus validates each typed pair in that list and binds evaluated steps by name.

For an API source set, api_integrity_check is available through the stdio MCP server, the browser’s WebMCP workbench, and the CLI’s yichus call. All three use the same Bosatsu tool catalog and checker. Pass the complete source set as sources and select the evidence format explicitly:

{"sources":[{"fileName":"model.bosatsu","source":"…"},{"fileName":"handlers.bosatsu","source":"…"}],"max_ops":8,"schema":"3.0","view":"compact"}

The top-level tool ok and WebMCP isError say whether the tool ran. They do not say that every property holds. Read each item in verdicts.claims.

What a claim means

In the compact view, operation numbers index the top-level operationCatalog. Each entry keeps its package, binding, source region, ordinal, effect kind and state reference. The compact diagnostic sketch supplies a hash and a request to retrieve the full view using the same source bytes. That sketch was not run by TLC.

A race claim with UnorderedWriteCapableSites means the bounded schedules permit different orders of operations that can write the cell; an unclassified or opaque effect also counts as write-capable. Allocating a next database ID advances state, so it counts as a write-side operation too. An unclassified effect with no known state reference makes a positive per-cell race claim inconclusive, because it might touch that cell. A violation does not claim the resulting cell values differ. The claim's scope lists the selected operations, bound, and explored schedule count.

identity.complete: false lists the missing compiler, builtin, registry, checker and runtime-adapter identities. trusts.tlcRun: false and trusts.leanRun: false are explicit: this native result is neither a TLC state-space result nor a Lean theorem. The separate api_lean_check method can produce a checked receipt for supported direct Bool and structural List[Bool] laws on a configured host. Its compact view points to the exact full receipt by digest; neither view upgrades a native Spec verdict or establish a system invariant.

Version transition

The default in the current 0.1.x line remains schema: "legacy-2.2" so existing verdict readers keep their wire format. The race-order predicate is corrected in both 2.2 and 3.0: read-only moves around a fixed write order no longer produce a race warning, while unordered ID allocations and unattributed effects no longer produce false positive race-freedom claims. This can change 2.2 outcomes, trace counts, and witness hashes for identical source; preserve an older artifact if exact historical output matters. Existing three-argument input-indexed transition declarations must add the matching literal handler name as their first argument; this prevents model steps from silently attaching to the wrong handler when a list is reordered. Use schema: "3.0" for typed claims. Version 0.2.0 will make 3.0 the default; version 0.3.0 is the planned removal release for the legacy selector. An internal 2.2 import primitive preserves a historical JSON tree but marks its missing origin, scope and completion as unknown; no public import command is available yet, and such records cannot satisfy a new evidence gate.

Choose another check · Tool schema · Try the state-machine demo