TLAPS: A TLA+ Proof System

The TLA+ Proof System (TLAPS) mechanically checks TLA+ proofs. The TLA+ proof language is declarative, hierarchical, and scalable to large system specifications. It provides a consistent abstraction over the various “backend” verifiers. The current release of TLAPS does not perform temporal reasoning, and it does not handle some features of TLA+. An extension to the full TLA+ language is under active development. However, TLAPS is now suitable for verifying safety properties of non-trivial algorithms.