From Wikipedia, the free encyclopedia
Jump to: navigation, search
Paradigm Action
Designed by Leslie Lamport
First appeared April 30, 1994; 21 years ago (1994-04-30)[1]
TLA+2 / January 15, 2014; 15 months ago (2014-01-15)[2]
Implementation language
OS Cross-platform (multi-platform)

TLA+ (styled as TLA+) is a formal specification language originally developed by Leslie Lamport for specifying concurrent and distributed systems and algorithms. It is based on the temporal logic TLA (also introduced by Lamport) for the description of the system's behavior and on standard set theory for representing data structures.

TLA+ specifications and their properties are both written as formulas in the same logical language. Specifications are organized in modules that contain declarations of variables and constants, definitions of operators, and assertions of assumptions and theorems.

Tool support for TLA+ includes the TLC model-checker, the TLA+ Proof System (TLAPS) and a PlusCal translator. All of them are integrated in the TLA+ Toolbox, an Eclipse-based IDE.

In addition, TLA+ is extended with a notation for writing hierarchical proofs, which can be interpreted by TLAPS.

See also[edit]


  1. ^ Lamport, Leslie (30 May 1994). "The Temporal Logic of Actions". ACM Transactions on Programming Languages and Systems (TOPLAS) (ACM) 16 (3): 872–923. doi:10.1145/177492.177726. 
  2. ^ Lamport, Leslie (15 January 2014). "TLA+2: A Preliminary Guide" (PDF). Retrieved 2 May 2015. 

External links[edit]