# 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¶

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