TLA+ and PlusCal Appetizer

“Temporal logic of actions (TLA) is a logic developed by Leslie Lamport, which combines temporal logic with a logic of actions. It is used to describe behaviours of concurrent systems.” [1]

TLA+ is a formal specification language built on top of the TLA logic. It is used to design and verify the correct behavior of programs and is especially useful in distributed and concurrent systems. PlusCal is a formal specification language as well that gets transcompiled to TLA+. It is used to specify algorithms.

Continue reading