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 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.
8. 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.