You'll miss a lot on this web site unless you enable Javascript
in your browser.
Introduction [show]
This page assumes you are familiar enough with TLA+ to be able to
understand a simple TLA+ spec (not just a PlusCal spec).
It contains links to documents explaining topics that go beyond what
most engineers need to know about TLA+.
These topics may be useful to engineers who want to push the boundary
of what they can do with TLA+, and they will be of interest to
those who want a deeper understanding of the principles underlying
TLA+.
Stuttering Steps [show]
It seems obvious to me that in any sensible definition of
implementation, a clock that displays hours, minutes, and
seconds should implement the specification of a clock that displays
hours and minutes.
I realized in 1983 that the simplest way to ensure that this is true
is to require that all specifications allow
stuttering steps—steps in which the state of the system does not change. Steps of an hour/minute/second clock in which only the seconds change implement stuttering steps of the hour/minute clock's specification. In the decades since then, I have continued to explain this to people. To my knowledge, no statebased specification formalism other than TLA has adopted the idea. I suspect that even many TLA+ users think it's weird to require that specifications allow stuttering steps. Here is a link to a short note explaining why not requiring it is weird: [a link]. I don't understand why many people write such weird specs. Safety, Liveness, and Fairness [show]
The terms safety, liveness, and
fairness are used informally throughout the TLA+
documentation—including in the
TLA+ Video Course. They are defined precisely
in this note, which also describes
their significance. Although it requires little knowledge of TLA+,
you might find the note to be tough going if you're not used to
reading mathematics. But it's worth the effort if you want a more
complete understanding of TLA+.
Proving Safety Properties [show]
I have been writing correctness proofs of concurrent algorithms for
about 45 years.
I developed what I find to be a natural way of writing these proofs.
However, writing rigorous proofs has remained a black art that few
people have mastered.
Learning to write these proofs starts with learning to write proofs
of safety properties.
I believe that TLA+ and its tools can help you learn to write
these proofs.
The document Proving Safety Properties
shows you how.
It explains the art of writing rigorous proofs, but not completely
formal machinechecked proofs.
Writing machinechecked proofs requires a lot of additional effort, as
well as practice using the TLAPS proof system.
Hiding, Refinement, and Auxiliary Variables [show]
I started thinking about writing specifications around 1980. I
quickly realized that it was important to understand what it meant for
a program to satisfy a spec. I knew that, in principle, a spec
and an executable program are both specifications of a physical
system, written at two different levels of abstractions. So, I
needed to understand what it meant for one specification to implement
or refine another. This ultimately led me to TLA, the temporal
logic underlying the TLA+ language, and to using the temporal
existential quantification operator (written
\EE in TLA+)
to write specifications. This operator served to distinguish
variables that represent externally observable parts of the system
from ones that represent unobservable parts that need not appear in an
implementation. Temporal existential quantification hid those
unobservablevariabled.
With the development of the TLA+ tools and seeing how TLA+ is used in
practice, I came to realize that engineers and computer scientists
didn't need the
While engineers don't need to use variable hiding and the

