Start with the question

The opening part earns the six ideas every later tool assumes. It is compact on purpose: the tools, not a second abstract-mathematics course, are the book's destination.

1. Choose the Question Before the Notation — state what the model answers and refuses.
2. Keep Only Differences That Change the Future — choose state by future observation, not stored fields.
3. One State Can Have Several Next States — preserve nondeterminism for the checker.
4. A Bad Future Leaves a Finite Scar — turn safety into a finite counterexample.
5. Eventually Borrows a Promise — expose the fairness assumption inside progress.
6. Green Has a Boundary — keep every result attached to its scope.

Describe behavior with TLA+ and TLC

1. Values Before Variables — build state from sets, functions, records, and sequences.
2. A Module Names Its World — separate fixed parameters, changing state, and definitions.
3. Actions Are Predicates Over Two States — encode steps without erasing nondeterminism.
4. Make the Forbidden State Executable — break and repair a safety invariant.
5. Give the Infinite Language a Finite Model — bind constants and run the negative control.
6. Read the Trace Backward — turn state deltas into a causal diagnosis.
7. Make the State Space Pay Rent — reduce exploration only with an observation-preservation argument.
8. Say Eventually Precisely — state eventuality and the fairness mechanism it borrows.

This lane is complete: it begins with values in an empty directory, constructs a module and actions, fails and repairs an invariant, configures TLC, diagnoses the trace, controls the state space, and ends with paired unfair and fair liveness models plus an unlike transfer to replicated configuration.

Search symbolically with Apalache

1. Types Make the Symbolic World Finite Enough — type the supported symbolic world before asking for a verdict.
2. Ask for the Whole Bounded Trace — search every admitted prefix through a declared length.
3. Strengthen What Must Survive One Step — separate initiation, preservation, and implication.

This lane keeps three boundaries distinct: type checking says the symbolic question is well formed; bounded checking excludes witnesses through one declared length; induction obligations can establish invariance when all three parts hold. Its unlike transfer is bounded resource conservation.

Model structure with Alloy

1. Everything Begins as a Relation — construct atoms, signatures, tuples, and fields.
2. Join Replaces the Pointer Chase — compose authorization paths with relational operators.
3. Run Finds a World; Check Finds a Refutation — interpret SAT and UNSAT by command kind.
4. A Small Scope Still Needs a Witness — retain scope, reject vacuity, and transfer to reified grants.

The checked model grades every command: the buggy assertion has a SAT counterexample, the fixed assertion is UNSAT within scope, and useful guest sharing remains SAT.

Execute the model with Stateright

1. Rust Can Be the Model — implement state, actions, and a pure transition relation.
2. The Checker Owns the Choices — explore admitted branches and read the shortest counterexample.
3. Put the Network in the Model — make delivery, loss, duplication, and timeout explicit.

The first checked model isolates Stateright's Model trait with a turnstile. The second moves to actors and finds the message order that makes a replicated register regress. A monotonic update repairs that specimen without pretending that bounded exploration verifies code or behavior omitted from the model.

Verify Rust code with Kani

1. A Harness Turns Values Symbolic — quantify over machine values and retain a failing control.
2. Assumptions Spend the Proof Domain — constrain inputs, cover intended cases, and justify loop unwinding.
3. A Contract Can Replace an Implementation — verify preconditions and postconditions before stubbing a body.

The checked numeric specimen first finds unsigned overflow in the familiar (low + high) / 2 midpoint. Its repair is proven over every ordered pair of u8 values. A bounded prefix loop and an experimental function contract then make assumptions, unwind completeness, reachability, and compositional proof obligations visible.

Explore local concurrency with Loom

1. Instrument the World You Want Explored — replace opaque synchronization with modeled primitives.
2. One Test Contains Many Schedules — reconstruct the lost update and repair the compound action.
3. Memory Order Is Part of the Claim — verify a release/acquire publication edge and retain Loom's limits.

The checked concurrency specimen requires two known failures: a load/store increment loses an update, and a relaxed readiness flag fails to publish its payload. fetch_add repairs the first; release/acquire synchronization repairs the second. Both controls and repairs run through the same pinned Loom 0.7.2 dependency used by the public Cargo project.

Finish with judgment

1. Choose by Question, Not Reputation — select and refuse tools by the shape of a claim.
2. Stack Evidence Without Blending It — complete an unfamiliar capstone and preserve every evidence boundary.

The first edition's route is complete. The final assessment is not a quiz about tool names. It asks you to split a one-use credential service into structural, behavioral, code, and local-schedule claims; select only the evidence each claim needs; retain negative controls; and write one argument that does not erase the gaps between model and implementation.

Each tool lane has the same completion test: begin from a blank public project, write the required forms, run a failing negative control, explain the witness, repair it, change the question, and construct an unlike transfer model.

Two speeds, one standard

The first-contact route takes the shortest path through the examples. “Under the hood” and “At scale” sections deepen the same model after the essential semantics are complete. Skipping those sections never excuses a vague result: every reader must still name the claim, assumption, bound, and forbidden inference.

Nothing here tracks progress. The finished edition supplies static one-day, one-week, and one-month retrieval routes. Progress remains something the reader can demonstrate, not something the site records.

Retrieve after the page is closed