Curry On Talk: The Practice and Theory of TLA+
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+.
There is a mistake in the slide at ~35:00. I neglected to add $\UNCHANGED N$. The $FactAlg$ spec should read:
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.”