The TLA+ Proof System (TLAPS) mechanically checks TLA+ proofs.
TLA+ is a general-purpose formal specification language that is particularly useful for describing concurrent and distributed systems. 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+.
At one point, Open Hub analyzed source code for this project based on code location(s) available at that time. Since then, the code locations have been removed.
30 Day SummaryNov 25 2017 — Dec 25 2017
12 Month SummaryDec 25 2016 — Dec 25 2017