pressron

$$\newcommand{\sc}[1]{\mathrm{\small{#1}}\;} \newcommand{\comment}[1]{\bbox[lightgrey,2pt]{\text{#1}}} \newcommand{\str}[1]{``\mathsf{#1}\!"} \newcommand{\nested}[1]{\!\!\rlap{\begin{aligned}\begin{alignat}{1}#1\end{alignat}\end{aligned}}} \newcommand{\set}[1]{\{#1\}} \newcommand{\seq}[1]{\langle #1 \rangle} \newcommand{\llbracket}{[\![} \newcommand{\rrbracket}{]\!]} \newcommand{\sem}[1]{\llbracket #1 \rrbracket} \newcommand{\H}{-\!\!\!} \newcommand{\UR}{\lower 4.3pt {\urcorner}\!\!} \newcommand{\UL}{\lower 4.3pt {\ulcorner}\!\!\!} \newcommand{\LR}{\raise 2.5pt {\lrcorner}} \newcommand{\LL}{\raise 2.5pt {\llcorner}\!\!\!} \newcommand{\defeq}{\triangleq} \newcommand{\E}{\exists\,} \newcommand{\A}{\forall\,} \newcommand{\EE}{\pmb{\pmb{\boldsymbol{\boldsymbol{\exists}}}}\,} \newcommand{\AA}{\pmb{\pmb{\boldsymbol{\boldsymbol{\forall}}}}\,} \newcommand{\implies}{\Rightarrow} \newcommand{\whileop}{\overset{+}{-}\!\!\triangleright\; } \let\savedBox=\Box \renewcommand{\Box}{\raise1mu{\small \square} } \renewcommand{\Diamond}{ {\Large \diamond} } \newcommand{\LET}{\sc{LET}} \newcommand{\IN}{\sc{IN}} \newcommand{\RECURSIVE}{\sc{RECURSIVE}} \newcommand{\LAMBDA}{\sc{LAMBDA}} \newcommand{\IF}{\sc{IF}} \newcommand{\THEN}{\sc{THEN}} \newcommand{\ELSE}{\sc{ELSE}} \newcommand{\CASE}{\sc{CASE}} \newcommand{\OTHER}{\sc{OTHER}} \newcommand{\CHOOSE}{\sc{CHOOSE}} \newcommand{\BOOLEAN}{\sc{BOOLEAN}} \newcommand{\TRUE}{\sc{TRUE}} \newcommand{\FALSE}{\sc{FALSE}} \newcommand{\DOMAIN}{\sc{DOMAIN}} \newcommand{\EXCEPT}{\sc{EXCEPT}} \newcommand{\STRING}{\sc{STRING}} \newcommand{\MODULE}{\sc{MODULE}} \newcommand{\LOCAL}{\sc{LOCAL}} \newcommand{\INSTANCE}{\sc{INSTANCE}} \newcommand{\WITH}{\sc{WITH}} \newcommand{\EXTENDS}{\sc{EXTENDS}} \newcommand{\ASSUME}{\sc{ASSUME}} \newcommand{\VARIABLE}{\sc{VARIABLE}} \newcommand{\VARIABLES}{\sc{VARIABLES}} \newcommand{\CONSTANT}{\sc{CONSTANT}} \newcommand{\CONSTANTS}{\sc{CONSTANTS}} \newcommand{\UNION}{\sc{UNION}} \newcommand{\SUBSET}{\sc{SUBSET}} \newcommand{\UNCHANGED}{\sc{UNCHANGED}} \newcommand{\ENABLED}{\sc{ENABLED}} \newcommand{\WF}{\text{WF}} \newcommand{\SF}{\text{SF}} \newcommand{\THEOREM}{\sc{THEOREM}} \newcommand{\LEMMA}{\sc{LEMMA}} \newcommand{\COROLLARY}{\sc{COROLLARY}} \newcommand{\PROPOSITION}{\sc{PROPOSITION}} \newcommand{\AXIOM}{\sc{AXIOM}} \newcommand{\PROOF}{\sc{PROOF}} \newcommand{\ASSUME}{\sc{ASSUME}} \newcommand{\PROVE}{\sc{PROVE}} \newcommand{\QED}{\sc{QED}} \newcommand{\BY}{\sc{BY}} \newcommand{\DEF}{\sc{DEF}} \newcommand{\DEFS}{\sc{DEFS}} \newcommand{\OBVIOUS}{\sc{OBVIOUS}} \newcommand{\OMITTED}{\sc{OMITTED}} \newcommand{\NEW}{\sc{NEW}} \newcommand{\STATE}{\sc{STATE}} \newcommand{\ACTION}{\sc{ACTION}} \newcommand{\TEMPORAL}{\sc{TEMPORAL}} \newcommand{\USE}{\sc{USE}} \newcommand{\DEFINE}{\sc{DEFINE}} \newcommand{\SUFFICES}{\sc{SUFFICES}} \newcommand{\HAVE}{\sc{HAVE}} \newcommand{\TAKE}{\sc{TAKE}} \newcommand{\PICK}{\sc{PICK}} \newcommand{\WITNESS}{\sc{WITNESS}} \newcommand{\HIDE}{\sc{HIDE}}$$

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

ERRATA:

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

   $$\begin{alignat}{1} &FactAlg \defeq \;& \LET fact[n \in Nat] \defeq \IF n \leq 1 \;\THEN 1 \;\ELSE n * fact[n - 1]\\ &&\IN N \in Nat \land f = 0 \land\; \Box[f' = fact[N] \land \UNCHANGED N]_{\seq{N, f}}\\ \end{alignat}$$

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