Learning TLA+ and Model Checking

• Specyfing systems: by Leslie Lamport is still the reference book for TLA+ and its tools

• The Specification Language TLA+: Another good manuscript by Stephan Merz explaining TLA+ specification language: Sect. 2 introduces TLA+ by way of a first specification of the resource allocator and illustrates the use of the tlc model checker. The logic TLA is formally defined in Sect. 3, followed by an overview of TLA+ proof rules for system verification in Sect. 4. Section 5 describes the version of set theory that underlies TLA+, including some of the constructions most frequently used for specifying data. The resource allocator example is taken up again in Sect. 6, where an improved high-level specification is given and a step towards a distributed refinement is made. Finally,Sect. 7 contains some concluding remarks

Resources

A collection of resources about TLA+ can be found on the awesome-tla+ repository. Feel free to contribute with your useful links.