LLMs can now generate TLA+ syntax, but you still need to understand temporal logic to define correctness and interpret results.
Key Takeaways
TLA+ (Temporal Logic of Actions) defines state machines as logical formulas; the model checker TLC does exhaustive BFS over all reachable states.
Frontier LLMs generate TLA+ specs from prompts, removing the syntax barrier while leaving the hard part (specifying what correctness means) to you.
Temporal operators <> (eventually) and [] (always) let you express liveness properties over entire behaviors, not just single-state invariants.
Infinite state spaces must be bounded in beans.cfg via constants like WMAX/BMAX before TLC can model-check; bounds come from engineering judgment.
The beans puzzle illustrates a key pattern: parity invariants (b % 2) survive all transitions, so termination outcomes are fully determined by initial conditions.
