Idea
Verification methods and their boundaries
From a check to a proof
Does this calculation give the right answer for every input? Can some sequence of operations reach a bad state? Tests show that the inputs you tried passed, which is less than either question asks. Here you state the property in Bosatsu and check it against the compiled code: by sampling inputs, by trying every value of a finite type, by searching a declared model, or by checking a theorem. Each of those answers a different question. Before relying on a result, check which inputs it covered, whether the check finished, and which translation step you are trusting.
Run a state-machine check →See a finite law check →
System property / Spec
Can a sequence of operations reach a bad state?
Available: yichus spec and api_integrity_check analyze causal order and explore bounded operation schedules. Their versioned evidence distinguishes a declared-model result from an implementation claim.
Still internal: a pinned TLC runner and translation of a closed, finite declared Bosatsu model. The public Spec commands do not run TLC. Even a completed TLC search of that model would not establish that the handlers implement it.
Run the current state-machine example →Function property / Law
Does a calculation obey a rule for every input?
Available: yichus law and api_law_check sample inputs or exhaust a supported finite type or explicit Bosatsu value list. The finite verdict names the accepted type or listed scope it covered.
A completed finite verdict is a local result from the trusted Yichus engine over the supplied source. The JVM CLI snapshots file bytes; MCP and WebMCP compile in-memory sources in killable workers. Re-run after changing the source or build. Read the finite-result trust boundary →
Available with a proof host: yichus lean and the configured npm MCP host recompile the source and ask pinned Lean to check generated law and witness theorems. Translation is limited to direct Bool laws and a structural List[Bool] shape. Browser-only WebMCP reports that a host is required.
What does each result establish?
Read the subject, method, scope, completion, and assumptions together. A sampled law says holds, a completed finite check says holds-exhaustive for its recorded scope, and a Lean proof receipt says proved. None of those labels alone links a declared model to its implementation.
Useful for finding concrete defects. A new input can still fail.
Complete for an enumerated type, or exactly the distinct values the author listed. An unfinished witness stays inconclusive.
The model, configuration, and missing implementation link limit the claim. A cutoff is inconclusive.
The receipt names the source, theorem, toolchain, and admitted Bosatsu-to-Lean translation.
The native Spec checker has its own structural and bounded methods; it is not a TLC run. Its versioned evidence is available through CLI, MCP, and WebMCP. A completed finite law check is only complete for its declared finite scope. A verified Lean receipt covers the supported type-wide theorem, subject to its recorded translator and toolchain assumptions.
How to read the evidence
A property written in Bosatsu is a statement of intent. Whether a result says something about a compiled function, a declared transition model, or a running service depends on the bridge the checker actually verified.
- Subject and bridge
- Find the named law or model. Finite and Lean law checks evaluate or translate a restricted compiled function closure. The TLC work searches a declared transition model; it does not yet prove that handlers implement that model.
- Method and scope
- Check whether inputs were sampled, a listed domain was exhausted, or a type-wide theorem was checked. For a Spec result, read the schedule and operation bounds. A small domain cannot discharge an all-input requirement.
- Completion
- Unsupported syntax, an unfinished witness, a budget cutoff, a missing host tool, or a timeout remains inconclusive. A tool call that completed successfully is not automatically a property that holds.
- Trust and identity
- A Lean receipt binds exact source bytes to the generated theorem and pinned toolchain for a local run. Acceptance across builds requires recompiling, regenerating, and rechecking; a copied receipt alone is insufficient.
For the exact tool requests, result shapes, and supported syntax, use the runnable examples and check chooser.
Try the checks
The state-machine demo lets you edit Bosatsu source and rerun the native Spec checker in the browser. Its verdict cards include the declared model and exploration bound. For a function law, inspect registration.bosatsu: its enrollment fold reads the opening seat count instead of the running count. From a checkout with the CLI built, run:
yichus law demos/laws/registration.bosatsuThe command exits nonzero for over-enrollment. In step, change seat_count(seats, class_id) to seat_count(acc, class_id) and rerun: the seeded check no longer finds that violation, but the unfinished WitnessTodo keeps the obligation inconclusive. To compare a completed finite check with a type-wide Lean proof, use the finite law and recursive List law examples.