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+.