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.
References
[1] https://www.youtube.com/watch?v=rkZzg7Vowao