writing-tla-plus-specs

Writing TLA+ specs

Contract

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.