Specifying and verifying systems with TLA+
Leslie Lamport, John H. Matthews, Mark R. Tuttle, Yuan Yu · 2002
TLA+ is a high-level specification language that has been used to specify and check the correctness of several hardware protocols. We expect that it can also be used to specify and check concurrent algorithms and protocols for software systems.