TLAPlus
TLA+ is a formal specification language for describing and verifying system behaviour mathematically. A system is modelled as a state machine; a model checker exhaustively explores all possible states to verify that safety properties (nothing bad happens) and liveness properties (something good eventually happens) hold. TLA+ has been used at Amazon Web Services, Microsoft, and Intel to catch subtle bugs in distributed system designs before implementation.
The conventional barrier to TLA+ adoption has been learning its syntax and mathematical notation. LLM-assisted TLA+ lowers this barrier: a developer describes the system in natural language, an LLM writes the TLA+ specification, and the model checker (TLC) verifies it. The human role shifts from specification author to specification reviewer.
Placed in Techniques > Assess at outer position because LLM-assisted formal specification is an emerging workflow rather than an established practice. The underlying technique (TLA+ model checking) is proven and well-documented; the LLM acceleration is newer and the quality of LLM-generated specs on complex systems is unproven. Worth exploring for teams building distributed systems where correctness properties are critical and informal reasoning has proven insufficient.
