TLA stands for the Temporal Logic of Actions, but it has become a shorthand for referring to the TLA+ specification language and the PlusCal algorithm language, together with their associated tools.

TLA+ is based on the idea that the best way to describe things formally is with simple mathematics, and that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely. TLA+ is especially well suited for writing high-level specifications of concurrent and distributed systems.

PlusCal is an algorithm language that, at first glance, looks like a typical tiny toy programming language. However, a PlusCal expression can be any TLA+ expression, which means anything that can be expressed with mathematics. This makes PlusCal much more expressive than any (real or toy) programming language. A PlusCal algorithm is translated into a TLA+ specification, to which the TLA+ tools can be applied.

The principal TLA+ tools are the TLC model checker and TLAPS, the TLA+ proof system. All the tools are normally used from the Toolbox, an IDE (integrated development environment). Go to the TLA home page to find out more about TLA.