- Specifying Systems
This is a comprehensive introduction and formal grounding of TLA+, though it has very little on model checking. Does not cover features past 2004 or so (like pluscal and Recursive Operators.
- TLA+ Video Course
A video course by the inventor of TLA+.
- Introduction to Formal Pragmatic Modeling
A fantastic dive into three large production-level specifications. Assumes some TLA+ knowledge.
- TLA+ Language Reference Manual
A formal reference by the developers of Apalache. Work in progress.
- TLA+ Version 2
Covers Recursive Operators and lambda expressions.
- Current Versions of the TLA+ Tools
Information on TLC flags if you run it from the command line, as well as the other tools (except PlusCal). Information on TLC module operators.
- Pluscal Manual
Formal definition of PlusCal, flags, and command line options. See f.ex the “label” option on page 70, which automatically generates the labels your spec needs.
- Summary of TLA+
A TLA+ cheat sheet. Includes some TLA+ constructs that none of the tooling can check, like action composition. Uses typeset symbols instead of ASCII ones (so \(\in\) instead of
- How Amazon Web Services uses Formal Methods
The paper that first got major companies interested in using TLA+. Also how I found out about it.
- TLA+ Example Repository
A collection of abstract algorithms and protocols.
- TLA+ in Practice and Theory
A detailed analysis of the mathematical theory that underpins TLA+.
- Let’s Prove Leftpad
A collection of proofs of leftpad in different formal methods. Not entirely related to TLA+ but <shameless plug here>
- TLA+ Community Modules
A collection of useful modules to add to the minimal TLA+ stnadard library.
An alternate model checker for TLA+. It uses symbolic model checking instead of enumerating all states.
(Disclosure, I’m currently doing some consulting work for Informal Systems.)