What is TLA+?

TLA+ is a language for creating “specifications” for computer programs/algorithms and then verify all the possible execution paths and mathematically prove assertions. The program is represented as a state machine where everything from variables to the program counter “pc” is part of the state. The spec contains an initial state and rule specifying “next state” as a bunch of logical statements linked by “and” (/) or “or” aka / clauses.


[1] https://www.youtube.com/watch?v=rkZzg7Vowao

[2] https://lamport.azurewebsites.net/video/intro.html


  • Computer Science