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.

Reference Material

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

Reading Resources

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>

Talks

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

Other Tooling

TLA+ Community Modules

A collection of useful modules to add to the minimal TLA+ stnadard library.

Apalache

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.

Community

The TLA+ Homepage

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.