TLA Proof System

Develop proof assistant for enabling certification of TLA+-expressed specification.

TLA+ is a specification language that, together with the associated Pluscal algorithm language has been proposed by Leslie Lamport as a method for developing and verifying algorithms for concurrent and distributed systems. The TLA+ tools have gradually matured, and have recently been used for industrial applications (in the US by Microsoft and Amazon engineers, and in France by CEA engineers). TLA+ has become one of the mainstream methods for specifying and checking properties of distributed systems.
An associated proof assistant is an important complement to model-checking for establishing properties of TLA+ specifications of algorithms. The development of such a proof assistant has been one of the first projects of the Joint Centre.
Although TLA+ and its foundations are well established, there is more to be learned about how it should be used in practice. Leslie Lamport and Stephan Merz have recently made a significant improvement to an approach first developed over 25 years ago.
There is still much work to be done on the proof assistant, especially for reasoning about liveness properties.