/tlaplus

name: tlaplus
description: Use to model-check real code or a design with TLA+ and TLC. Model retries, locks, async flows, protocols or state machines as written, check invariants over every interleaving, and reproduce any counterexample trace as a failing test. Dispatched by /engineer.harden for concurrency- and ordering-shaped risks; also usable directly, including to spec a design before building it. Triggers — "/engineer.tlaplus", "use TLA+ to verify X", "model-check X for races/deadlocks", "write a TLA+ spec for this protocol".

TLA+

TLA+ earns its keep by finding the counterexample you didn't think of. Don't write a spec and declare victory without actually running TLC — an uncompiled/unchecked spec is just prose with extra syntax.

Setup check

`java -version` (TLC needs a JVM 11+; if it's missing, tell the user rather than installing one). The model checker jar (`tla2tools.jar`, pinned to v1.7.4) auto-downloads on first run via `${CLAUDE_PLUGIN_ROOT}/skills/tlaplus/scripts/tlc.sh`, no separate install step needed.

Translating an informal design into TLA+

When the user describes a protocol/state machine in plain language, structure the spec around these pieces — this is the actual translation work, not boilerplate:

1. **`VARIABLES`** — the pieces of state that change. Keep this minimal; every variable multiplies the state space TLC has to explore. 2. **`Init`** — the starting state predicate. 3. **Actions** — one predicate per state transition (e.g. `SendMsg`, `Crash`, `Receive`). `Next == SendMsg \/ Receive \/ Crash \/ ...` 4. **Invariants** — the safety properties that must hold in *every* reachable state (e.g. `NoDataLoss`, `MutualExclusion`). These are what TLC actually checks — a spec without invariants can't find bugs. 5. **(Optional) Temporal properties** — liveness, e.g. `EventuallyDelivered`, checked separately from safety invariants and much more expensive.

Ask the user what actually must never happen (safety) before modeling — that answer is the invariant, and it's the one thing you can't infer from the protocol description alone.

Workflow

1. Write `Spec.tla` (the spec/module) and `Spec.cfg` (which invariants to check, `CONSTANTS` values, and state-space bounds like a max number of processes — TLC exhaustively explores states, so unbounded constants mean it never finishes). 2. Run: `bash ${CLAUDE_PLUGIN_ROOT}/skills/tlaplus/scripts/tlc.sh Spec.tla Spec.cfg` 3. **Read the output precisely.** TLC either says the invariant holds (`Model checking completed. No error has been found.`) or prints a counterexample trace — the exact sequence of states that breaks the invariant. That trace is the whole value of doing this: don't summarize it away, show the state-by-state trace so the actual bug is visible. 4. Fix the spec (or realize the invariant was wrong) and rerun. A "violation" is sometimes the invariant being stated too strongly — check which one is actually wrong before patching either. 5. If TLC times out or the state space is too large, narrow `Spec.cfg` constants (fewer processes/values) first — that's usually cheaper than restructuring the spec, and still finds most bugs since TLA+ bugs are rarely scale-dependent.

Verifying real code ("use TLA+ to verify X")

This is a different job from writing a spec from scratch: the goal is finding real concurrency/protocol bugs in real code and getting them fixed. The `.tla` files are scaffolding, not the deliverable — nobody merges them, they merge the PRs the counterexamples led to. TLA+'s specific strength here is interleavings: races, missed locks, out-of-order delivery, retry/timeout interactions — the class of bug that's nearly impossible to hit with a unit test because it depends on *when* two things happen relative to each other. Reach for TLA+ over Lean when the suspected bug is about concurrent/ interleaved behavior; reach for Lean when it's about a pure functional transformation or an unbounded data invariant. Structure the work as a todo list and post progress as you go — this runs long.

1. **Split the target into independent state machines**, same as for a from-scratch spec — read the real source and model each orthogonal subsystem (retry logic, session lifecycle, a message queue, a lock protocol) as its own small `.tla` module. 2. **Model from the code as written, not as intended.** States, actions, and guards must mirror the actual implementation including its bugs, or every check is vacuous. Cite the file/line each action is based on. 3. **State the invariants a reviewer would actually care about** (mutual exclusion, no lost message, bounded retries, no state stuck unreachable) and check them with TLC. TLC's exhaustive search over the bounded state space in `Spec.cfg` is doing the same job proof search does in Lean, but it's automatic — you don't have to find the counterexample yourself, TLC does, which is exactly why this is a good fit for "does this race exist." 4. **Review each model independently against the real code before trusting its results.** A clean TLC run on a wrong model proves nothing about the real system. 5. **When TLC reports a violation, don't report the abstract trace as the finding — reproduce it against the real code.** Translate the state-by-state trace into a concrete interleaving/input sequence and confirm it against the actual implementation (a test, a script forcing the interleaving, or a careful read of the code path). If it doesn't reproduce, the model diverged from reality — fix the model, not the code. 6. **For every confirmed bug, pin it with a test that fails before the fix and passes after.** State it in those terms: the test is what proves the bug was real and the fix works. Opening a PR is an external write. Propose the draft PR and wait for the human's OK (`${CLAUDE_PLUGIN_ROOT}/references/handoff-dispatch.md`). When `/engineer.harden