TLA+ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems. TLA+ is considered to be exhaustively-testable pseudocode,[4] and its use likened to drawing blueprints for software systems;[5] TLA is an acronym for Temporal Logic of Actions. For design and d