Example
Bounded Interleaving Verification for Bosatsu State Machines
Spec-first development for Bosatsu state machines. You declare the properties first and fill in the handlers, then read native checker verdicts instead of re-checking the state machine in your head. TLC integration is not available yet. How to read the versioned evidence.
A Yichus/Spec declaration models a state cell as a transition system and states
properties as ordinary pure Bosatsu functions. yichus spec extracts
IO operations, state cells, and causal order from typed IR, then applies the spec's declared
transition rows while exploring interleavings within a bound. The operation-to-transition
binding is currently declared-only, so the transition model can drift from a
handler's write payload; the checker does not yet derive that correspondence from IR. It reports
a three-valued verdict per property:
holds, violated (with a source-located counterexample trace), or
inconclusive (with the reason).
Each JSON artifact on this page is regenerated by running the checker against the sources shown,
on every deploy of this site. None of the verdicts below is a screenshot. The three scenarios
follow the submission lifecycle of the agora incubator app. The domain FSM allows
Received → Processing → BriefReady → Judging → Ranked → Archived (with failure paths),
and Archived is terminal. The domain source is below. Every property on this page
bottoms out in its can_transition, so read that first.
submission.bosatsu: the domain FSM (can_transition, is_terminal)
loading…
To run any of the commands below (needs git, a JVM 17+, and
sbt). The alias must be defined at the repository
root, because $(pwd) is expanded when you define it; the commands themselves run
one directory down, which is what domain/, specs/ and
fixtures/ are relative to:
git clone https://github.com/snoble/yichus
cd yichus
sbt assembly # writes target/scala-*/yichus.jar
alias yichus="java -jar $(pwd)/target/scala-*/yichus.jar"
cd yichus-agoraHow to read a verdict
Each property gets one card: the verdict word, the property name, where it was declared, and the reason. The three verdicts are exhaustive and mean exactly this:
| Verdict | Meaning within the declared model and bound |
|---|---|
| holds | The property was true at every step of every interleaving the checker enumerated,
and nothing was left unexplored (0 truncated). Conclusive within the
bound, and only about the declared model. |
| violated | At least one interleaving drives the model through a step where the property is false. A counterexample trace is attached. |
| inconclusive | The checker refused to answer: a write it could not model, a declared operation with no implementation, or operations past the bound. An unexplored case is never reported as holding. |
The colour repeats the word; it carries nothing on its own. A word in a section heading summarises that scenario in this page's words, and is not a verdict the checker emitted. That is why two of them use words outside the verdict vocabulary: mixed means the scenario's cards disagree and the command exits nonzero, and interactive just marks the section you can run yourself.
Reading a counterexample trace. Steps print in the order the interleaving
runs them, but each #N is the operation's fixed identity in program order, so
the numbers legitimately appear out of sequence (#0, #2, #1 means the third
operation ran before the second). Each line gives the binding, the primitive
(read/write), the cell and its file:line:column;
traces for declared properties also carry the model state that step produces. Built-in race
traces leave that off, because a race is about ordering rather than the modeled state.
Coverage line. “Explored N interleaving(s) within a bound of 8 ops
(0 truncated)”: an op is one IO operation on the modeled cell, and reads count as
well as writes. The bound caps the total number of operations the checker will
consider across the whole program, rather than limiting each handler separately. Sites past
it are dropped, counted as truncated, and force inconclusive. So 0 truncated
is what makes a holds conclusive here. --max-ops N changes it, up to a
hard ceiling of 8.
The two built-in invariants. causal-consistency checks that
every ordering the checker explored respects the happens-before relation it derived from
the code's flat_map/sequence composition. That is a self-check on
the enumeration, so it holds unless the checker itself is wrong.
race-free:<cell> reports that different legal orderings of that cell
produce different effect sequences: a lost-update hazard, independent of any property
you declared.
Where stale-read: cards come from. The checker re-runs each
declared property under read-capture semantics and emits a
stale-read:<property> card only when the property survives atomic
steps but breaks under read capture. Existing verdicts never change silently; the
stale read gets its own card. That is why only-legal-steps has one below and
terminal-is-final does not.
What fails a build. A violated declared property
always exits nonzero. No flag is needed. Built-in invariants
(causal-consistency, race-free:<cell>) are diagnostics and
never gate. --require-holds a,b adds a second demand: the named
properties must be conclusively holds, so an inconclusive also fails. That
is what stops a spec with no handlers from passing CI silently.
--output <path> writes the JSON artifact the cards are rendered from; the
native check and violation gate also run when output goes to stdout. stale-read:<property> cards
count as declared properties, so a violated one does gate; section 3 below is
exactly that case.
1. Day 0: spec first, no handlers yet (inconclusive)
The spec declares two operations and two step-properties before any handler exists. Every property reports inconclusive, because the obligations are registered and nothing has been discharged. It is the same moment as a type signature whose body is still a stub.
yichus spec domain/submission.bosatsu specs/submission.spec.bosatsu --output verdicts.jsonsubmission.spec.bosatsu: the spec (guarded model + properties)
loading…Loading verdicts…
2. Unguarded handlers: violated, with a trace
Three handlers each write their target state unconditionally. Any one of them looks innocent on
its own, but under interleaving they drive the FSM through illegal transitions. The checker finds
the orderings and reports them as counterexample traces, with every step source-located and
annotated with the model state it produces. Watch the second trace resurrect an
Archived submission. The CLI exits nonzero, so a CI run fails on it.
yichus spec domain/submission.bosatsu specs/submission_unchecked.spec.bosatsu fixtures/intake_handlers_unchecked.bosatsu --output verdicts.json
# exit 1intake_handlers_unchecked.bosatsu: the handlers
loading…submission_unchecked.spec.bosatsu: the spec (models the handlers as written, as constant setters)
loading…Loading verdicts…
3. Guarded handlers: mixed result, declared properties hold, a stale read still gates
The fixed handlers read the current state and write only when the domain's
can_transition allows the move. The spec models them with the same compiled
can_transition function the handlers call. The
Transition rows that associate operations with those step functions are still
declared rather than verified (see the declared-binding soundness limits). Every interleaving is explored, and under
atomic steps both declared properties hold.
The command still exits nonzero, and that is the point of this section.
Guarding fixes the atomicity bug and exposes a deeper one: the third card below,
stale-read:only-legal-steps, is violated. A read-check-write handler
decides on the value it read; if another handler moves the state between that read
and the write, the decision is stale and an illegal step slips through. That card is a
declared property, so it gates. A guard on its own is not enough, and the checker says so
even though the cards above it are green.
yichus spec domain/submission.bosatsu specs/submission.spec.bosatsu fixtures/intake_handlers_guarded.bosatsu --output verdicts.json --require-holds only-legal-steps,terminal-is-final
# exit 1 — only-legal-steps and terminal-is-final hold, but stale-read:only-legal-steps is violatedintake_handlers_guarded.bosatsu: the handlers
loading…Loading verdicts…
race-free diagnostic still flags that
the two handlers race on submission_state, since different orderings produce different
effect sequences (a lost-update hazard). The atomic FSM properties hold under every one of those
orderings; the read-capture property finds an illegal stale step. Generic races and
domain-property violations are different questions, and the verdict
artifact answers both, side by side.
Run the checker in your browser (interactive)
The same checker, compiled to JavaScript, running entirely in your browser. Below is a fresh
example: a door that must be unlocked (Locked → Closed) before it can be opened
(Closed → Open), three handlers (two guarded, plus a force_open that
writes unconditionally), and a spec that models all three as written. Check it, then edit the code
and check again. Things to try:
- See the bug: check as-is, and
only-legal-movesis violated byforce_openfiring while the door is stillLocked. - Fix it: guard
force_openlike the other handlers (read, checkcan_move, then write) and change its model step in the spec to the guarded form. The verdict flips to holds. - See the deeper bug the guard does not fix: after the fix, a separate stale-read:only-legal-moves card is violated. A read-check-write handler decides on the value it read; if another handler moves the door between its read and its write, the decision is stale and an illegal move slips through. The counterexample trace shows the exact interleaving. holds (each step applied atomically) and this violation are both true, because they model different things.
- See the soundness rules: delete only the
force_openhandler (leaving itsTransitiondeclared) and the verdict is inconclusive: declared operation not implemented. Delete aTransitionrow while its handler still writes and you get inconclusive: unmodeled write. An unexplored case is never reported as holding.
door_spec.bosatsu: the spec
Work with your agent
WebMCP connects your agent to this page. Connection and tool instructions. Use yichus_page_feedback to read the current editor and displayed feedback. The agent can use yichus_page_edit to update the current source and yichus_page_action to run a listed button, then read feedback for completion and diagnostics. Autocomplete suggestions remain available for you to accept with Tab.
door_handlers.bosatsu: the handlers
door.bosatsu: the domain FSM
These editors support agent autocomplete over WebMCP: pause typing or press Ctrl+Space, then Tab to accept the suggestion.
Typed-IR extraction, declared transition binding, and soundness limits
Yichus’s supported effect operations return typed IO[A] values. The checker identifies IO-typed expressions and registered primitives from the typed IR. External implementations must honor that contract. It extracts modeled IO sites and state references, derives the
happens-before relation from flat_map/sequence composition, enumerates
the valid interleavings (independent cells commute and are pruned), applies the spec's declared
transition at each modeled write, and evaluates the spec's properties at every step. Those
properties are compiled by the same compiler as the implementation.
Soundness rules: an unmodeled write to the cell, an unimplemented declared operation, or operations
beyond the exploration bound keep verdicts inconclusive. No verdict claims more than was
explored.
The model-to-implementation binding is currently declared rather than verified (verdicts carry
modelBinding: declared-only); verifying declared steps against write payloads in the
IR is the next milestone.
Read more: the design brainstorm · the specs and fixtures on GitHub · raw artifacts: day 0, unguarded violation, guarded mixed result.
Where this fits
What this is about: Checks and Proofs