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 · All the Ways It Can Break

growing

Choose by Question, Not Reputation

The most sophisticated tool in the room can still answer the wrong question precisely.

formal-methods, tool-selection, verification, modeling, engineering-judgment, learn

You will classify claims by mathematical shape, choose a default tool, name a credible alternative, and refuse a tool when its green result would answer only a nearby question.

Start with the claim shape

This table records the default fit taught in this book. It is a routing aid, not a claim that a tool is incapable of neighboring work.

Question shape Default route Typical witness Result boundary
State changes, nondeterminism, safety, or fairness TLA+ with TLC reachable state trace or temporal counterexample the configured finite model and encoded behavior
A typed TLA+ safety claim through length k, or an induction obligation Apalache symbolic bounded trace or failed proof obligation supported fragment, types, length, and invariant strength
Atoms and relations admit or forbid a structure Alloy satisfying instance or assertion counterexample finite scope and model facts
An executable Rust model includes messages, timers, and faults Stateright path of model actions modeled state, actions, faults, and search boundary
A Rust function is safe for every admitted finite machine value Kani symbolic counterexample and playback value compiled harness, assumptions, checks, and unwind completeness
Local instrumented threads have a failing schedule Loom schedule-sensitive assertion failure instrumented primitives, modeled memory behavior, and exploration bounds

TLC and Apalache both consume TLA+ but do not produce interchangeable evidence. TLC explicitly explores states in a configured finite model. Apalache uses symbolic techniques over its supported typed fragment and can discharge bounded or induction-shaped obligations. Choose by the obligation, then record the checker.

TLA+ and Stateright both describe transition systems. TLA+ keeps the model close to mathematics and temporal logic. Stateright keeps it executable in Rust and offers an actor/network vocabulary. Choose the representation whose gap and exploration behavior you can audit—not the syntax your team happens to know.

Refusal is part of competence

A good selection sentence includes a rejection:

Use Alloy for the finite authorization relation and its counterexample.
Do not use this check as evidence about revocation order over time; that is a separate behavioral claim.

Common wrong turns reveal the boundary:

  • Adding more unit tests does not enumerate protocol schedules.
  • Encoding an authorization graph as procedural transitions can obscure the relation the property quantifies over.
  • Using Kani on one parser function does not prove a distributed service's liveness.
  • Using Loom on an uninstrumented standard-library lock does not explore that lock.
  • Using a finite TLC model or Alloy scope does not produce an unbounded theorem.
  • Using a Stateright actor because the implementation uses actors does not prove the implementation corresponds to the model.

These are not arguments against the tools. They prevent their valid results from being attached to invalid conclusions.

Selection — choose the question before the familiar tool.

Split compound requests

“Verify the service” is not one question. Rewrite it as a claim ledger:

  1. only owners and invited readers can reach a document;
  2. a canceled operation never later publishes;
  3. accepted byte lengths never index past a buffer; and
  4. two local claimants never both win one token.

Those claims naturally route to different evidence. Some may need only tests or review, not a formal tool. The ledger prevents a prestigious result for Claim 3 from becoming vague confidence in Claims 1, 2, and 4.

Cost and correspondence decide ties

When two tools fit, compare:

  • how directly the notation expresses the property;
  • whether the desired witness is legible;
  • which bounds make exploration feasible;
  • how much production behavior must be re-modeled;
  • whether the team can independently rebuild and maintain the artifact; and
  • which unsupported semantics remain decisive.

The smallest adequate model usually creates the clearest evidence. More tools and more detail can increase cost while decreasing the visibility of the actual claim.

Lessons

  • Classify the claim before choosing notation or checker.
  • Tool overlap does not erase differences in witness and proof boundary.
  • A selection is incomplete until it names a credible refusal.
  • Split “verify the system” into independently falsifiable claims.
  • Similar names between model and code do not establish correspondence.
  • The smallest adequate evidence portfolio is stronger than a pile of green badges.

Practice

  1. Retrieval. Reconstruct the six rows of the routing table without looking.
  2. Discrimination. Why might both TLA+ and Stateright fit one protocol, yet produce different engineering costs?
  3. Transfer. Split a rate limiter into at least three claims and choose evidence for each, including one explicit refusal.

Worked answers

  1. Behavior/TLC, typed symbolic TLA+/Apalache, structure/Alloy, executable distributed model/Stateright, finite Rust paths/Kani, local schedules/Loom.
  2. They differ in notation, temporal vocabulary, executable-model proximity, fault libraries, checker behavior, state representation, and the correspondence work required.
  3. Example: token-bucket arithmetic to Kani; concurrent in-process updates to Loom; refill and distributed ownership behavior to TLA+ or Stateright. Refuse the Kani arithmetic proof as evidence of scheduler fairness.

References

  1. Leslie Lamport. The TLA+ home page. — behavioral specification and tools
  2. AlloyTools. Alloy. — relational modeling and analysis
  3. Kani. Kani Rust Verifier. — code-level bounded model checking
  4. Loom. Loom 0.7.2. — instrumented concurrency testing and its limits

← Memory Order Is Part of the Claim Stack Evidence Without Blending It →