TLA+ Spec Generator

Turn a prose description of a concurrent or distributed system into a TLA+ module that TLC can actually check. The hard part is not TLA+ syntax — it is deciding what belongs in the state and what doesn't.

Step 1 — Decide if TLA+ is the right tool

TLA+ is for: nondeterminism, concurrency, message-passing, protocols, state machines — anything where interleaving matters.

TLA+ is not for: sequential algorithms, data-structure invariants within one thread, arithmetic correctness, type-level properties. For those → cpp-to-dafny-translator or → c-cpp-to-lean4-translator.

Rule of thumb: if the bug you're afraid of requires two things happening "at the same time," use TLA+. If it's "this function returns the wrong value," don't.

Step 2 — Extract state variables

Read the description and mark every noun that persists across steps and can be observed. These become VARIABLES.