You're viewing the readable version of this site. The interactive extras (search, diagrams, read-aloud) need JavaScript and a current browser. Enable JavaScript; if it is already enabled, update your browser.

Learn · Workshop book

budding

Before the Machine Acts

Learn formal modeling by finding failures in real system designs.

formal-methods, web-security, concurrency, distributed-systems, agents, learn

You need software engineering experience and no formal-methods background. By the final workshop, you will be able to write and run a small TLA+ model, use TLC and Apalache without confusing their claims, explore a Rust state machine with Stateright, search a trust graph with Alloy, prove a Rust kernel with Kani, and expose local thread schedules with Loom.

Each lab names the checker version its result was produced with, and the Loom lab pins Loom 0.7.2 in its own lockfile, so the printed output is reproducible rather than approximate. The labs are small on purpose. Each lab isolates one design decision that also appears in larger systems.

The workshop route

  1. Model a Checkbox — learn state, actions, invariants, and enough TLA+ to write a first machine.
  2. Check Every Reachable State — run TLC, read a counterexample, and repair the transition.
  3. Ask a Solver for the Trace — run Apalache on the same TLA+ and state its bound honestly.
  4. Explore a Rust Protocol — use Stateright to check stale spreadsheet publication.
  5. Draw the Browser Trust Graph — use Alloy to reason about Content Security Policy.
  6. Retry an Uncertain Commit — model a Datastore-style lost reply without duplicating an effect.
  7. Prove the Admission Kernel — use Kani to cover every approval and request value in a Rust harness.
  8. Explore the Lost Update — use Loom to expose a local concurrency failure.
  9. Design the Evidence Stack — combine the tools for an agent control system without merging their claims.

How to use the book

Run each command before reading the trace explanation. Change the named defect before opening the worked answer. Keep a small notebook with four lines per lab: claim, admitted behavior, excluded behavior, and remaining risk.

Each command invokes one tool directly, from the directory holding the model file the lab shows you. Save that file under the name printed above the command and the command runs as written. You will need TLA+'s tla2tools.jar for the TLC labs, Apalache for the symbolic lab, Alloy for the trust graph, and a Rust toolchain with Kani for the proof lab; the Stateright and Loom labs run under cargo test in a crate that lists the library as a dependency.

What the book does not promise

The workshops teach working fluency, not mastery of each language. The models do not verify a browser, a cloud database, Rust's memory model, or an agent runtime as a whole. Each result covers the property, abstraction, assumptions, and bounds printed beside the command. That sentence is part of the result.