TLA+ Formal Specification Skill

Write non-trivial TLA+ specifications, run the TLC model checker, and bridge the gap between formal specs and implementation code.

Setup (Run Once)

bash SKILL_DIR/scripts/setup.sh

This downloads tla2tools.jar (v1.8.0) and verifies Java 11+. The JAR is stored at SKILL_DIR/lib/tla2tools.jar.

Quick Reference

Load the right reference for your task:

Task	Reference
TLA+ syntax, operators, types	references/language.md
PlusCal syntax, processes, labels	references/pluscal.md
Distributed systems patterns	references/patterns/distributed-systems.md
Protocol specifications	references/patterns/protocols.md
Invariants, safety, liveness	references/patterns/invariants.md
Code ↔ spec mapping, bug finding	references/patterns/code-to-spec.md

Load references on-demand — read the ones relevant to the current task before writing any spec.

Templates

Start from a template when creating a new spec:

Template	Use For
templates/basic.tla	Pure TLA+ state machine
templates/pluscal.tla	PlusCal algorithm with processes
templates/distributed.tla	Distributed system with messages

Running Specs

Full Check (Recommended)

Translates PlusCal (if present), parses, and model-checks in one step:

bash SKILL_DIR/scripts/check.sh spec.tla --config spec.cfg

Individual Tools

# Parse only (syntax check)
bash SKILL_DIR/scripts/parse.sh spec.tla

# Translate PlusCal to TLA+
bash SKILL_DIR/scripts/translate.sh spec.tla -nocfg

# Model check with TLC
bash SKILL_DIR/scripts/tlc.sh spec.tla --config spec.cfg --workers auto
bash SKILL_DIR/scripts/tlc.sh spec.tla --no-deadlock    # suppress deadlock check

Direct Java Invocation

JAR="SKILL_DIR/lib/tla2tools.jar"

# Parse
java -cp "$JAR" tla2sany.SANY spec.tla

# Translate PlusCal
java -cp "$JAR" pcal.trans -nocfg spec.tla

# Model check
java -cp "$JAR" tlc2.TLC -workers auto -config spec.cfg spec.tla

# REPL
java -cp "$JAR" tlc2.REPL

# Dump state graph (for visualization)
java -cp "$JAR" tlc2.TLC -dump dot,actionlabels,colorize states.dot spec.tla

Workflow: Writing a Spec

1. Understand the System

Before writing any TLA+:

• Identify the concurrent agents (processes, nodes, threads)
• Identify shared mutable state (queues, databases, locks, counters)
• Identify the key safety property ("what must never happen?")
• Identify the key liveness property ("what must eventually happen?")

2. Choose PlusCal vs Pure TLA+

Use PlusCal when:

• The system is naturally sequential/imperative
• You're modeling code (threads, goroutines, async tasks)
• You need await, while, goto semantics
• The audience is programmers

Use Pure TLA+ when:

• You need fine-grained fairness control
• The system is naturally a state machine
• You need interruptible/restartable actions
• You need refinement mappings
• A single label would need to update a variable twice

3. Start Small, Then Expand

1. Write the simplest possible spec that captures the core behavior
2. Add a type invariant immediately
3. Run TLC with small constants (2-3 nodes, 2-3 messages)
4. Add safety invariants one at a time, running after each
5. Add liveness properties with fairness
6. Increase constants to expand coverage

4. Config File

Every spec needs a .cfg file. Create one alongside the .tla:

SPECIFICATION Spec

\* Properties to check
INVARIANT TypeInvariant
INVARIANT Safety

\* Uncomment for liveness (slower)
\* PROPERTY Liveness

\* Constants
CONSTANT
  NumNodes = 3
  MaxMsgs = 5
  NULL = NULL

\* Uncomment to bound state space
\* CONSTRAINT StateConstraint

\* Uncomment to ignore deadlocks
\* CHECK_DEADLOCK FALSE

Workflow: Spec From Code

When the user has existing code and wants a spec:

1. Read the code — understand concurrency structure, shared state, synchronization
2. Read references/patterns/code-to-spec.md
3. Map constructs — threads→processes, locks→await, channels→queues
4. Abstract — don't model every line, only concurrency-relevant operations
5. Write spec — start with the concurrent skeleton, add detail iteratively
6. Run TLC — find deadlocks, invariant violations, liveness failures
7. Report — translate any TLC error traces back to code execution paths

Workflow: Finding Bugs

When comparing a spec to code, or looking for bugs:

1. Read references/patterns/code-to-spec.md
2. Write a spec modeling the suspected buggy area
3. Run with small constants — TLC is exhaustive, small state space is fine
4. Interpret error traces — map TLA+ state sequences to code execution paths
5. Check atomicity — does the code do atomically what the spec's label does?
6. Check completeness — does the code handle all either/or branches?
7. Check ordering — does the code enforce the same happens-before relations?

If TLC finds a violation:

• The error trace is a concrete counterexample — a specific sequence of events
• Map each state in the trace to concrete code state
• The transition that causes the violation is the bug location

Interpreting TLC Output

Success

Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val: 0

Invariant Violation

Error: Invariant SafetyInvariant is violated.
The following behavior constitutes a counter-example:
State 1: <Initial predicate>
  /\ var1 = ...
State 2: <Action line X>
  /\ var1 = ... (changed values in red)

Deadlock

Error: Deadlock reached.

→ No process can make progress. Check await conditions and process completion.

Liveness Violation

Error: Temporal properties were violated.

→ Check fairness settings. Add WF_vars or SF_vars. Trace may include a "stuttering" suffix.

Key Principles

1. Type invariants first — catch spec bugs before checking real properties
2. Small constants — 3 nodes finds most bugs; 10 nodes takes 1000× longer
3. Safety before liveness — invariants are faster to check
4. One property at a time — add incrementally, run after each addition
5. Fairness is opt-in — TLA+ assumes everything can crash by default
6. => with \A, /\ with \E — never use => with \E
7. Sequences are 1-indexed — always
8. Every action must specify all variables — use UNCHANGED for untouched ones