Skip to content


TLA+ is a formal specification language developed to design, model, document, and verify concurrent systems.


  1. tlaplus Public

    TLC is an explicit state model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

    Java 1.6k 122

  2. Examples Public

    A collection of TLA+ specifications of varying complexities

    TLA 789 128

  3. Dr. TLA+ series - learn an algorithm and protocol, study a specification

    TLA 606 70

  4. tlapm Public

    The TLA Proof Manager

    OCaml 26 9

  5. TLA+ snippets, operators, and modules contributed and curated by the TLA+ community

    TLA 138 20

  6. PlusPy Public

    Python interpreter for TLA+ specifications

    Python 84 5


Top languages


Most used topics