alt Hacker News> 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, and its use likened to drawing blueprints for software systems;
In theory (according to Wikipedia at least) the acronym stands for "Temporal Logic for Actions" ... but the pun in the standard meaning of the acronym TLA (i.e. "Three Letter Acronym") is far too enticing for me to believe the choice was fully accidental. :D