Other Resources¶

Learning Resources¶

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 \in).

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>

Designing Distributed Systems with TLA+: My standard pitch talk for using TLA+.
Weeks of Debugging can save you Hours of TLA+: Markus (the core toolbox developer)’s pitch talk for using TLA+.

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

TLAPS: A proof system for TLA+ if you want to use it as a theorem prover.

VSCode plugin: For if you want to run TLA+ outside of the toolbox, but not in the command line.
TLA2JSON: Does exactly what it says it does. There’s plans to add this feature to the toolbox, but that isn’t ready yet.
tree-sitter-tlaplus: The Treesitter parser-generator.

conf.tlapl.us: The standard site where we put info on our annual TLA+ conference. Usually cohosted with Strange Loop.
TLA+ Google Group: This is where all the core developers hang out and answer people’s questions.
r/tlaplus: The TLA+ subreddit.