yichus dist checks a modeled distributed system against declared safety properties by exploring the delivery schedules the network could produce. The model (a “world”) is written in Bosatsu, the pure total language everything on this site compiles: named nodes, each a pure handler (state, sender, msg) -> Step(next_state, sends). Handlers cannot do IO, so every source of nondeterminism belongs to the checker: which in-flight message is delivered next, and which faults occur. A violated property is reported as a concrete schedule with every node’s state after each event; holds is reported only when exploration covered every schedule.
A world declares its nodes, a fault budget, and its properties. The fault budget is three integers: how many messages the network may drop, how many deliveries it may duplicate, and how many nodes may crash. Properties are pure Bosatsu functions over all node states — the spec and the implementation share one compiler. For example, the property that both increments landed once traffic settles:
def both_counted(views: List[NodeView[WState]]) -> Bool:
eq_Int(db_value(views), 2) # db_value reads the db node's counter
world = DistSpec(
World([Node("db", ...), Node("app1", ...), Node("app2", ...)]),
FaultBudget(0, 0, 0), # drops, duplicates, crashes
[Invariant("never-overcounted", ...)], # checked after every event
[FinalInvariant("both-counted", both_counted)], # checked when no messages remain
describe_state, describe_msg)
Databases, retrying clients, supervisors are all just nodes in the world file; the checker itself is only a scheduler, the fault budgets, and property evaluation. Running it:
yichus dist protocol.bosatsu checker.bosatsu solution.bosatsu --verdicts out.json
Each property comes back holds, violated (with the schedule), or inconclusive. The exit code is nonzero on any violation, so the command gates CI.
The checker runs a depth-first search over schedules, bounded by a maximum events-per-schedule (default 12) and a cap on total schedules. If every schedule ends with no messages in flight before hitting either bound, exploration is complete and holds is permitted. If any schedule was cut off, the run is truncated: violations found are still real, but unviolated properties report inconclusive, never holds. Beyond the bound the checker also runs seeded random schedules; a violation found there replays exactly from its seed. Completeness also implies termination: a complete run means every schedule reached quiescence, so a final property cannot pass vacuously on a system that never settles.
One committed task models a web service writing to a database: two app servers each add 1 to a shared counter through a versioned store (Get returns value and version, Put writes blindly, Cas writes only if the version still matches). The fault budget is zero — delivery order is the only adversary. A server that reads and writes back blindly passes every sequential test; under the schedule where both servers read before either writes, one increment is lost. The checker's output for that server (states shown as db(v=value, ver=version)):
1. deliver app1 -> db [Get] db(v=0,ver=0) app1(waiting) app2(waiting) 2. deliver app2 -> db [Get] db(v=0,ver=0) app1(waiting) app2(waiting) 3. deliver db -> app1 [GotValue(0,0)] db(v=0,ver=0) app1(done) app2(waiting) 4. deliver db -> app2 [GotValue(0,0)] db(v=0,ver=0) app1(done) app2(done) 5. deliver app1 -> db [Put(1)] db(v=1,ver=1) app1(done) app2(done) 6. deliver app2 -> db [Put(1)] db(v=1,ver=2) app1(done) app2(done) quiescent; both_counted requires v == 2, found v == 1: violated
The compare-and-swap version of the same server satisfies all properties over all 106 schedules — 106 being every legal interleaving of this world’s messages (two request/reply conversations plus CAS retries, zero faults) — and the run is complete, so holds is conclusive.
The worked example above has no attacker — delivery order is the only adversary. The checker also models an active attacker on the wire. You add an AdversaryNode to the world. The checker then explores every attacker move, not only every delivery order.
AdversaryNode(name, init, on_start, on_message)
on_message returns a finite List[Step] — the attacker's move menu at that point. The checker explores every move in the menu, at every step, to the schedule bound. A property that comes back holds under an adversary means one thing: no attacker strategy in the modeled move space breaks it.
The attacker reasons over symbolic crypto terms (register DD26). Three constructors describe what it can and cannot do:
Clear(v) is plaintext. The attacker reads v.Sealed(v) is a ciphertext. The attacker carries it but cannot open it.Mac(dir, over) is a keyed tag. Only a key-holder makes one. dir binds the tag to a direction, so an initiator's tag and a responder's tag are distinct.The attacker's knowledge grows by a stated learn rule: it learns v from a Clear(v) term and learns nothing from a Sealed(v) term. It can replay any term it has seen. It cannot mint a Mac or open a Sealed without the key.
Three committed tasks check three attacks. Each ships a secure reference and a defective reference; the checker clears the first and catches the second. Run each the same way:
yichus dist protocol.bosatsu checker.bosatsu reference/solution.bosatsu --verdicts out.json
| Task | Attack | Secure reference | Defective reference |
|---|---|---|---|
| 008 forgery-auth | Replay a signature into a different session | injective-agreement holds (218 schedules, complete) | broken-unbound.bosatsu violated |
| 009 secrecy-transit | Read a secret off the wire | secret-confidential holds (2 schedules, complete) | broken-cleartext.bosatsu violated |
| 010 reflection-auth | Reflect the server's own nonce into a second session | mutual-authentication holds (13641 schedules, complete) | broken-reflectable.bosatsu violated |
Task 010 models a two-party mutual-authentication handshake over direction-tagged MACs. Mac(0, ·) is the initiator's proof; Mac(1, ·) is the responder's. The server under test is the responder. The secure server answers with Mac(1, ·) and accepts only Mac(0, ·), so the two directions never share a tag.
The defective server answers and accepts the same tag, Mac(0, ·). The attacker opens its own session and challenges the server with the server's own nonce. The server answers Mac(0, nonce) — a tag the keyless attacker cannot compute itself. The attacker replays that tag to finish a second session. The checker reports the schedule: the server records the forged session as authenticated while the honest client finished nothing. The defect exists only across two interleaved sessions, which is why a single-session read misses it.
The reflection task carries a down-tier reviewer benchmark. A weaker model (haiku tier) was asked to judge the reflectable server as secure or vulnerable. Without the checker it read the source and returned SECURE — a false certification. Its written argument even noted the shared tag, then reasoned that the attacker could not obtain it, and cleared the server. With the checker's counterexample in front of it, the same model returned VULNERABLE and reconstructed the cross-session oracle. A control cell cleared the secure server correctly, so the baseline is blind to the defect, not indiscriminate. Read it with the sample size in mind: three cells, one trial each, about 19.9k tokens per cell. It is an existence result, not a rate — a defect a cheaper model certifies from source and rejects when the checker's schedule is present. Full run data is in benchmarks/dist/results/iteration-009.md.
The standing benchmark result. Three defective variants of the correct compare-and-swap server were produced by an adversarial generator (an AI agent instructed to make each variant fail the checker while reading as correct; each variant's defect is confirmed by the checker before use). Fresh reviewer agents — no prior contact with this project — were asked to judge the three variants, plus the world files and the execution-model reference, as correct or defective. One trial per cell; two model sizes; with and without the checker:
| Reviewer | Without the checker (reading only) | With the checker |
|---|---|---|
| Stronger model | 3/3 caught, correct schedules derived by hand | — (not run; reading already suffices at this size) |
| Weaker model | 2/3 — certified one defective variant as correct, high confidence | 3/3 caught, root causes taken from the checker's schedules |
The variant the weaker reviewer accepted re-reads after a failed compare-and-swap and treats “the counter reached my target” as “my increment landed” — unsound, because a peer’s increment is indistinguishable from your own. The reviewer walked that exact schedule in its written argument and still judged the code correct. With the checker it reached the right verdict on the same file at roughly the same cost (37.9k vs 34.1k tokens of agent usage; each full checker run on this world takes seconds). The token and minute figures throughout are the reviewer agent’s total usage and wall-clock for the whole judging task.
Read with the sample size in mind: one trial per cell, two model sizes. What it demonstrates is an existence result, not a rate: there is a class of concurrency defect that a cheaper model confidently certifies from source and correctly rejects when the checker’s schedule is in front of it. At this world size (about 60 lines per variant) the stronger model catches these defects by reading; whether that survives larger worlds is not yet measured.
A benchmark like this fails silently if its property set is satisfiable without solving the problem. Two defenses are built into the committed tasks. First, hardcoding is caught in the model: the store node audits every committed write and latches a flag on any jump that is not exactly +1, behind its own invariant — a solution that fakes the final counter fails it. Second, reachability assertions: Sometimes("some-job-dispensed", check) declares that at least one explored state must satisfy the predicate; a spec whose invariants all hold while nothing ever happens reports violated on its coverage instead of passing. Both defenses are ordinary declarations in the world files, and each committed task ships known-bad variants that CI checks stay caught.
There are two implementations of the checker. The reference runs on the JVM and interprets the compiled Bosatsu handlers. The second compiles the world to JavaScript through the same code generator the site’s demos use and runs the search in Node.js — about 24× faster on the worked example above (0.3s vs 7s for its full exploration), with an optional visited-state cache that collapses redundant schedules. A differential test in CI runs both on the same worlds and requires identical per-property verdicts and identical schedule counts, which doubles as a conformance check on the JavaScript code generator. The same defect class is also caught at a different granularity by yichus tla, the single-process checker that explores interleavings of reads and writes inside one program's IO; the lost update above, rewritten as two service handlers sharing a state cell, fails its stale-read analysis the same way.
World files, tasks, known-bad variants, and per-run data: benchmarks/dist/ in the repository, with the execution model specified in benchmarks/dist/SEMANTICS.md.