TLA+
TLA+ is a formal specification language used to design, model and verify systems
TLA stands for the Temporal Logic of Actions, but it has become a shorthand for referring to the TLA+ specification language and the PlusCal algorithm language, together with their associated tools.
TLA+ is based on the idea that the best way to describe things formally is with simple mathematics, and that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely. TLA+ is especially well suited for writing highlevel specifications of concurrent and distributed systems.
PlusCal is an algorithm language that, at first glance, looks like a typical tiny toy programming language. However, a PlusCal expression can be any TLA+ expression, which means anything that can be expressed with mathematics. This makes PlusCal much more expressive than any (real or toy) programming language. A PlusCal algorithm is translated into a TLA+ specification, to which the TLA+ tools can be applied.
The principal TLA+ tools are the TLC model checker and TLAPS, the TLA+ proof system. All the tools are normally used from the Toolbox, an IDE (integrated development environment). Go to the TLA home page to find out more about TLA.
TLA+ 2018 Projects

Parv Mor
CONCURRENT ONTHEFLY SCCBASED LTL MODEL CHECKINGProject aims at implementation and proof of concurrent onthefly SCC detection algorithm to aid in liveness checking of TLC model checker. The goal...