tlaplus

TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

A collection of TLA+ specifications of varying complexities

Dr. TLA+ series - learn an algorithm and protocol, study a specification

Python interpreter for TLA+ specifications