requirement-to-tlaplus-property-generator
Installation
SKILL.md
Requirement → TLA+ Property Generator
A requirement is a claim about behavior. A TLA+ property is the same claim, stated precisely enough to check. The translation is about finding the formal shape of an informal statement.
Step 1 — Classify: safety or liveness?
| The requirement says… | It is… | TLA+ form |
|---|---|---|
| "never", "always", "must not", "at most" | Safety | Invariant: Inv == ... |
| "eventually", "will", "responds", "terminates" | Liveness | Temporal: Prop == <>... or []<>... |
| "if X then eventually Y" | Liveness (response) | [](X => <>Y) or X ~> Y |
| "X until Y" | Safety-ish | Encoded with history variables or LTL-style |
Safety = something bad never happens. Checkable at each state. Liveness = something good eventually happens. Needs fairness; checkable only over infinite traces.
Step 2 — Find the state predicate
Every property bottoms out in a predicate over state variables. Extract the nouns from the requirement; map them to VARIABLES.