program-to-tlaplus-spec-generator
Installation
SKILL.md
Program → TLA+ Spec Generator
TLA+ models state machines, not code. The translation isn't line-by-line — it's "what are the states, and what are the atomic transitions between them?" This is an abstraction exercise.
Step 1 — Identify the state
What persists between steps? That's your VARIABLES.
| Code construct | TLA+ variable |
|---|---|
| Shared mutable state (locks, queues, counters) | Direct — queue, lock_holder |
| Per-thread/process local state | A function: pc \in [Proc -> {"idle", "waiting", "cs"}] |
| Network messages in flight | A set or bag: msgs \subseteq Message |
| The program counter | A pc variable per process — where in the code each one is |
Do not model: pure function arguments, loop counters that don't cross await points, anything that's deterministic from the rest.