TLA+ Language Reference Manual 📗

In this manual, we summarize our knowledge about TLA+ and about its treatment with the Apalache model checker. This is not the manual on Apalache, which can be found in Apalache manual. The TLA+ Video Course by Leslie Lamport is an excellent starting point, if you are new to TLA+. For a comprehensive description and philosophy of the language, check Specifying Systems and the TLA+ Home Page. There are plenty of interesting talks on TLA+ at TLA Channel of Markus Kuppe. This manual completely ignores Pluscal -- a higher-level language on top of TLA+. If you are interested in learning Pluscal, check by Hillel Wayne.


  1. The standard operators of TLA+ 🔌
  2. User-defined operators 💡
  3. Modules and instances: MODULE, EXTENDS and INSTANCES ✂