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
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- Drive Quint when the spec is written in Quint. Run
quint typecheck spec.qnt, then quint run spec.qnt --invariant=NoDoubleSpend --max-steps=20 --max-samples=10000 for random simulation, then quint verify spec.qnt --invariant=NoDoubleSpend --max-steps=10 for the Apalache-backed bounded check (--backend=tlc selects TLC). quint run prints [violation] with the trace on failure; --out-itf writes the trace as an ITF file. Done when: the same property classification as step 5 is recorded.
- Record the result. State the tool, version, configuration, bound, state count or step length, and wall time beside each property. A property checked at three processes and depth 10 is proven at that instance and nothing more; write the bound next to the claim. Done when: every property line in the output carries its bound.
Failure and recovery
On a parse error, TLC exits 150 for the spec and 151 for the config; fix the reported line, then rerun. On state-space explosion (TLC exit 152, or a run that does not finish), shrink the constants, add a VIEW operator that abstracts state, or move to Apalache; do not lower the property. On an Apalache Type checker [FAILED] line, fix the @type annotation at the reported file and line; an untyped operator is a spec defect, not a tool limit. On a liveness violation whose trace ends in a stuttering loop, add the missing fairness condition and rerun; if the design has no fair action that makes progress, that is the finding. On an Alloy check that reports a counterexample, read the instance in the visualizer and reduce the scope until the smallest failing instance is found. TLAPS (tlapm) is a proof checker for TLA+ and is not a path this skill drives: its last stable release is 1.5.0 (2022-10-04) and 1.6.0-pre is marked pre-release; when a proof rather than a model check is required, say so and hand off. When a property cannot be checked at any useful bound, report the bound reached and the reason; do not weaken the property to make the run pass.
Output
Spec files (.tla with .cfg, .qnt, or .als) on disk; per property, a result line naming the engine, version, bound, and outcome; for each violation, the saved trace, its classification (spec bug, property bug, or design defect), and the fix applied or the defect handed to the design owner.
1---2name: writing-tla-plus-specs3description: 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.4---56# Writing TLA+ specs78## Contract910| Field | Bound contract |11|---|---|12| 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. |13| 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. |14| Side effect | Spec and configuration files on disk, plus TLC's `states` directory and Apalache's `_apalache-out` directory. |15| 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. |1617## Inputs1819A 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.2021## Procedure22231. 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.242. 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.253. 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.264. 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.275. 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.286. 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.297. Drive Quint when the spec is written in Quint. Run `quint typecheck spec.qnt`, then `quint run spec.qnt --invariant=NoDoubleSpend --max-steps=20 --max-samples=10000` for random simulation, then `quint verify spec.qnt --invariant=NoDoubleSpend --max-steps=10` for the Apalache-backed bounded check (`--backend=tlc` selects TLC). `quint run` prints `[violation]` with the trace on failure; `--out-itf` writes the trace as an ITF file. Done when: the same property classification as step 5 is recorded.308. Record the result. State the tool, version, configuration, bound, state count or step length, and wall time beside each property. A property checked at three processes and depth 10 is proven at that instance and nothing more; write the bound next to the claim. Done when: every property line in the output carries its bound.3132## Failure and recovery3334On a parse error, TLC exits 150 for the spec and 151 for the config; fix the reported line, then rerun. On state-space explosion (TLC exit 152, or a run that does not finish), shrink the constants, add a `VIEW` operator that abstracts state, or move to Apalache; do not lower the property. On an Apalache `Type checker [FAILED]` line, fix the `@type` annotation at the reported file and line; an untyped operator is a spec defect, not a tool limit. On a liveness violation whose trace ends in a stuttering loop, add the missing fairness condition and rerun; if the design has no fair action that makes progress, that is the finding. On an Alloy `check` that reports a counterexample, read the instance in the visualizer and reduce the scope until the smallest failing instance is found. TLAPS (`tlapm`) is a proof checker for TLA+ and is not a path this skill drives: its last stable release is 1.5.0 (2022-10-04) and 1.6.0-pre is marked pre-release; when a proof rather than a model check is required, say so and hand off. When a property cannot be checked at any useful bound, report the bound reached and the reason; do not weaken the property to make the run pass.3536## Output3738Spec files (`.tla` with `.cfg`, `.qnt`, or `.als`) on disk; per property, a result line naming the engine, version, bound, and outcome; for each violation, the saved trace, its classification (spec bug, property bug, or design defect), and the fix applied or the defect handed to the design owner.
OutlineDriven