Specifying and Verifying Systems With TLA+
Leslie Lamport, John Matthews, Mark Tuttle, and Yuan Yu

---

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.