The Specification Language TLA+

Abstract

The specification language TLA+ was designed by Lamport for formally describing and reasoning about distributed algorithms. It is described in Lamport's book Specifying Systems [29], which also gives good advice on how to make the best use of TLA+ and its supporting tools. Systems are specified in TLA+ as formulas of the Temporal Logic of Actions, TLA, a variant of linear-time temporal logic also introduced by Lamport [27]. The underlying data structures are specified in (a variant of) Zermelo-Fränkel set theory, the language accepted by most mathematicians as the standard basis for formalizing mathematics. This choice is motivated by a desire for conciseness, clarity, and formality that befits a language of formal specification where executability or efficiency are not of major concern. TLA+ specifications are organized in modules that can be reused independently.