page_title: TLA+
section_title: IDE
hierarchical_section_title: TLA+ / Tools / IDE
caption_attribution_description: English: Screenshot of TLA+ IDE 1.5 in typical use, showing spec explorer on the left, editor in the middle, and parse errors on the right. Depicted software is FOSS, licensed under MIT (see https://tlaplus.codeplex.com/license).
context_page_description: TLA⁺ is a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify programs, especially concurrent systems and distributed systems. TLA⁺ has been described as exhaustively-testable pseudocode, and its use likened to drawing blueprints for software systems; TLA is an acronym for Temporal Logic of Actions.
  For design and documentation, TLA⁺ fulfills the same purpose as informal technical specifications. However, TLA⁺ specifications are written in a formal language of logic and mathematics, and the precision of specifications written in this language is intended to uncover design flaws before system implementation is underway.
  Since TLA⁺ specifications are written in a formal language, they are amenable to finite model checking. The model checker finds all possible system behaviours up to some number of execution steps, and examines them for violations of desired invariance properties such as safety and liveness. TLA⁺ specifications use basic set theory to define safety and temporal logic to define liveness.
  TLA⁺ is also used to write machine-checked proofs of correctness both for algorithms and mathematical theorems.
context_section_description: An integrated development environment is implemented on top of Eclipse. It includes an editor with error and syntax highlighting, plus a GUI front-end to several other TLA⁺ tools:
  The SANY syntactic analyzer, which parses and checks the spec for syntax errors.
  The LaTeX translator, to generate pretty-printed specs.
  The PlusCal translator.
  The TLC model checker.
  The TLAPS proof system.
  The IDE is distributed in The TLA Toolbox.
caption: TLA+ IDE in typical use showing spec explorer on the left, editor in the middle, and parse errors on the right.
exif: {}