Curry On Talk: The Practice and Theory of TLA+

The full series about the theory of TLA+: Part 1, Part 2, Part 3, Part 4

If you find TLA+ and formal methods in general interesting, I invite you to visit and participate in the new /r/tlaplus on Reddit.

Here is my Curry On talk about TLA+.


  1. There is a mistake in the slide at ~35:00. I neglected to add $\UNCHANGED N$. The $FactAlg$ spec should read:

  2. In 26:24, I say “function” (twice!) when I mean to say “action”. It should be: “every time we have the box operator followed by an action, that action must be inside square brackets.”