/writing-tla-plus-specs

name: writing-tla-plus-specs
description: 'Use when a protocol, concurrent algorithm, or design needs a model-checked TLA+ or Alloy spec, or a TLC or Apalache trace needs reading. Not for choosing when to model: use validation-first-driven.'

Writing TLA+ specs

Contract

| Field | Bound contract | |---|---| | Trigger | A distributed protocol, concurrent algorithm, or system design needs an explicit-state or symbolic model check of its safety and liveness properties, or an existing TLC, Apalache, Quint, or Alloy run needs its counterexample read and acted on. | | Authority | Reversible local: writes `.tla`, `.cfg`, `.qnt`, and `.als` files and the tool output directories they produce; rollback is deleting those files. No remote mutation. | | Side effect | Spec and configuration files on disk, plus TLC's `states` directory and Apalache's `_apalache-out` directory. | | Done | Every named invariant and temporal property either passes under a recorded bound and configuration, or has a counterexample trace mapped to a named design defect. |

Inputs

A description of the system: its state variables, the actions that change them, and the properties that must hold. The tool pins from the grounded set: `tla2tools.jar` v1.7.4 (stable; v1.8.0 is a pre-release and the old TLA+ Toolbox GUI is declared unmaintained, so use the `tlaplus.vscode-ide` extension or the command line), Apalache v0.62.2 (download `apalache.zip` or `apalache.tgz` from GitHub Releases), Alloy v6.2.0 (standalone `.jar` from alloytools.org), Quint 0.32.0 (install per https://quint-lang.org/docs/getting-started). A JVM is required for TLC, Apalache, and Alloy. Optional: a state-space bound, a `ConstInit` operator that bounds constants for Apalache, and a Quint spec when the author prefers its surface syntax.

Procedure

1. Pick the engine. Use TLC when the model has a small finite instance and the properties include liveness. Use Apalache when constants are unbounded or the explicit state space is too large, and the properties are safety invariants or bounded temporal checks. Use Alloy when the question is about a data or relational structure rather than a protocol's steps; Alloy 6 adds `always`, `eventually`, `after`, `before`, `until`, and `releases` for temporal checks, and that mode requires NuSMV or nuXmv on `PATH`. Use Quint only as an alternate front end: it keeps TLA semantics and hands checking to Apalache or TLC through `quint verify`. Done when: one engine is named with the reason. 2. Write the spec skeleton. In TLA+, declare `CONSTANTS` and `VARIABLES`, define `Init`, one operator per action, `Next` as their disjunction, `Spec == Init /\ [][Next]_vars`, and a `TypeOK` invariant that names the domain of every variable. Keep every action a conjunction of a guard and primed assignments. For Apalache, annotate every constant and variable with `\* @type: T;` (types `Bool`, `Int`, `Str`, `Set(T)`, `Seq(T)`, `<<T1, T2>>`, `T1 -> T2`, `{ f: T }`) and run `apalache-mc typecheck Spec.tla` until it prints `Type checker [OK]`. In Alloy, declare `sig` and `fact` blocks, one `pred` per operation, and `run p for N` or `check a for N` commands; the scope keyword `for` bounds each signature. Done when: the spec parses and `TypeOK` holds in the initial state. 3. State the properties. Safety goes in invariants: one operator per claim, named for the claim (`NoDoubleSpend`, not `Inv1`). Liveness goes in temporal formulas under a fairness assumption (`WF_vars(Action)` or `SF_vars(Action)`) in `Spec`; without fairness every liveness property fails on a stuttering behavior. Done when: every property in the design brief has an operator, and every liveness formula has the fairness it needs. 4. Configure and run TLC. Write `Spec.cfg` with `SPECIFICATION Spec`, `CONSTANTS Name = Value` for each constant at a small instance (two or three processes first), `INVARIANTS TypeOK NoDoubleSpend`, and `PROPERTIES Liveness`. Run `java -jar tla2tools.jar -config Spec.cfg -workers auto Spec.tla`. Add `-deadlock` only when the spec models a terminating system and deadlock is not a defect; otherwise TLC treats a state with no successor as an error. Use `-simulate num=1000` for a quick random pass before an exhaustive run, and `-dfid N` for depth-first search of a deep state space. Done when: TLC exits 0 with the state count recorded, or exits 11 (deadlock), 12 (invariant violation), or 13 (temporal property violation) with a trace. 5. Read the TLC trace. The trace starts with `Error: Invariant X is violated` followed by `State 1:` through `State n:`, each listing every variable and the action that produced it. Read the last state first: the violated invariant names the variable that went wrong. Walk backward to the first action whose guard was too weak. Use `-difftrace` to print only changed variables, and `-dumpTrace json trace.json` to save the trace for a diff against the next run. Classify the cause as a spec bug (the action does not model the system), a property bug (the invariant is stronger than the design promises), or a design defect. Only the third is a finding for the design owner. Done when: the trace is classified and the defect or spec fix is written down. 6. Scale with Apalache. When TLC cannot finish, run `apalache-mc check --inv=NoDoubleSpend --length=10 Spec.tla`; `--length` bounds the number of steps and defaults to 10. Bound constants with `--cinit=ConstInit` where `ConstInit == N \in 2..5`. Check an inductive invariant with two runs: `--init=IndInv --inv=IndInv --length=0` proves the initial state satisfies it, and `--init=IndInv --next=Next --inv=IndInv --length=1` proves every step preserves it. Counterexamples land in `_apalache-out/` (override with `--out-dir`) as `counterexample1.tla`; `--max-error=N` collects up to N of them. Switch the backend with `--smt-solver=cvc5` when Z3 stalls. Done when: the property holds at the recorded bound, or the counterexample is classified as in step 5. 7. Drive Quint when the spec