Checking distributed systems by exhaustive simulation

A bug in a distributed system often shows up only in one order of events. Two servers read a shared counter, both add 1, both write back, and one increment is lost, but only when both reads land before either write. What if a message is dropped, delivered twice, or a node crashes? A test run sees one order, and a reviewer tracing the orders by hand can miss the bad one.

We built yichus dist to try every order up to a bound. You write the system as a model in Bosatsu. Each node's handler is shaped (state, sender, msg) -> Step(next_state, sends), returning its next state and outgoing messages as data. The checker tries every delivery order and declared fault up to the bounds you set, then evaluates the properties you supply. When one fails, you get the schedule that caused it.

See a lost update caught →See the reviewer benchmark →

What a holds result does and does not mean

A holds result is relative to the model, its initial state, and its configured fault choices; it is not a proof about every deployment of the protocol. Bosatsu checks recursion in language-defined functions, but external implementations remain trusted. A finite handler does not imply a finite conversation: nodes may keep sending messages. Exhausted search bounds therefore produce inconclusive, not a holding result.

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 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, and supervisors are nodes in the world. The three input files have distinct roles. protocol.bosatsu defines shared message, state, and step types. checker.bosatsu supplies the world, node implementations, fault budget, and properties. solution.bosatsu supplies the handler under review. The checker compiles all three together, schedules the resulting pure handlers, and evaluates the declared properties:

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. yichus dist guide prints the shapes a world is written in, the companion declarations the checker discovers by type (coverage, extra invariants, supervision, adversaries), and a complete example; the API MCP's api_guide carries the same section.

Bounded exhaustive search: completeness, truncation, and seeded walks

The checker runs a depth-first search over schedules. Defaults are 12 events per schedule, 20,000 exhaustively explored schedules, 100 seeded random walks after truncation, and 80 events per seeded walk. If every schedule ends with no messages in flight before either exhaustive bound, exploration is complete and holds is permitted. If any schedule is cut off, the run is truncated: violations found are still real, but unviolated properties report inconclusive, never holds. A seeded violation replays from its recorded seed. Completeness also implies termination: every schedule reached quiescence, so a final property cannot pass vacuously on a system that never settles.

Task 002 worked example: prevent a lost update with compare-and-swap

The committed task 002 directory models a web service writing to a database. Two app servers each add 1 to a shared counter through a versioned store. Get returns the value and version, Put writes blindly, and Cas writes only if the version still matches. The fault budget is zero, so delivery order is the only adversary. A blind read and write-back passes sequential tests but loses one increment when both servers read before either writes. The checker's output for that server shows states 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. Those schedules are every legal interleaving of two request/reply conversations plus CAS retries with zero faults. The run is complete, so holds is conclusive. The task 002 measurement record documents the two-arm run and checker result.

From a checkout, build the assembly and run the committed reference solution with the task's exact paths:

git clone https://github.com/snoble/yichus
cd yichus
sbt assembly
java -jar target/scala-*/yichus.jar dist \
  benchmarks/dist/tasks/002-lost-update/protocol.bosatsu \
  benchmarks/dist/tasks/002-lost-update/checker.bosatsu \
  benchmarks/dist/tasks/002-lost-update/reference/solution.bosatsu \
  --max-schedules 500000 \
  --require-holds never-overcounted,both-counted \
  --verdicts out.json

The exact scheduler, activation, fault, and property rules are in the Dist world semantics reference. Replace the solution path with reference/broken-blind-write.bosatsu to reproduce the six-event violation shown above.

Active-adversary worlds branch over finite attacker moves

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 and 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 no attacker strategy in the modeled move space breaks it.

The attacker reasons over symbolic crypto terms. 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

Reflection attack mechanics: cross-session use of a shared direction tag

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 also records a down-tier reviewer comparison. A weaker model (haiku tier) was asked to judge the reflectable server as secure or vulnerable. The recorded artifact has three cells and runs one trial in each. Each cell cost about 19.9k tokens. The first cell gave the model the source alone, the second added the checker's counterexample schedule, and the third was a control cell on the secure variant. The artifact does not record exact model IDs. Three trials establish that the case exists; they do not establish a rate.

Without the checker the haiku-tier reviewer 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, showing that this reviewer accepted the secure variant as well as missing the defective one. The three trials do not establish general reviewer reliability. The full run data is in iteration-009.md (served copy of benchmarks/dist/results/iteration-009.md).

Benchmark: reviewer accuracy with and without the checker

The standing benchmark uses three defective variants of the correct compare-and-swap server. An adversarial generator made each variant fail the checker while reading as correct, and the checker confirmed each defect before use. Fresh reviewer agents with no prior contact with this project judged the three variants, the world files, and the execution-model reference as correct or defective. The table runs one trial per cell. It has two model tiers, and each tier is judged twice, once with the checker and once without it. The recorded artifact names the tiers default tier, which was the coding harness's default model tier at the time, and haiku tier, which was its smaller tier. The artifact does not record exact model IDs, so these labels make no claim beyond those two recorded tiers:

Reviewer	Without the checker (reading only)	With the checker
Default-tier reviewer	3/3 caught, correct schedules derived by hand	not run; reading already suffices at this size
Haiku-tier reviewer	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”. This is 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 the table with its sample size in mind. Each cell is a single trial, so this is an existence result rather than a rate. It shows that there is a class of concurrency defect a cheaper model confidently certifies from source, and correctly rejects once the checker’s schedule is in front of it. At this world size, which is about 60 lines per variant, the stronger model catches these defects by reading alone. Whether that holds for larger worlds is not yet measured.

Benchmark validity: write-audit invariants and reachability coverage

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.

JVM and Node engines: differential scope and measured timing

There are two implementations of the checker. The reference runs on the JVM and interprets compiled Bosatsu handlers. The second compiles the world to JavaScript through the same code generator used by the site demos and runs the search in Node.js. On task 001, the recorded run measured about 24× faster execution (0.3s vs 7s for full exploration); the measurement register records those timings and the differential harness provides the reproduction path. An optional visited-state cache collapses redundant schedules. CI requires identical per-property verdicts for safety and final invariants, plus identical schedule counts and completeness on non-memoized runs. Sometimes coverage verdicts are excluded because only the JVM engine computes them. This also checks the JavaScript code generator. The same defect class is caught at a different granularity by yichus spec, the native 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.

Model size, property scope, and recovery limits

• Worlds are small. A world holds a few nodes and tens of messages. Larger fault budgets multiply schedules quickly, and the visited-state cache described above exists only in the JavaScript implementation so far.
• The checker covers safety and reachability only. It has no liveness properties beyond “complete exploration reached quiescence.”
• A crashed node stays crashed unless the world declares a supervisor for it. Recovery is modeled as a supervisor node whose restart message the checker may deliver to the crashed node (a Supervision(supervisor, node, restart) link); the restarted node’s own handler runs on the state it crashed with and decides what survives. A supervised node is always restarted before the schedule counts as settled. The checker has no restart of its own beyond that delivery.
• Properties observe node states, not message history; anything a property needs must be visible in some node’s state.

Browse the task and result tree, the task 002 inputs and variants, and the task 002 result record. Their repository paths are benchmarks/dist/ and benchmarks/dist/SEMANTICS.md. For a concrete bounded run and its counterexample, read the served task 010 run artifact; it records the fault budget, schedule count, complete holding reference, violated reflectable variant, and the limits of its one-trial reviewer comparison.