Title: Auxiliary Variables in TLA+,
Abstract: Auxiliary variables are often needed for verifying that an implementation is
correct with respect to a higher-level specification. They augment the formal
description of the implementation without changing its semantics--that is, the
set of behaviors that it describes. This paper explains rules for adding
history, prophecy, and stuttering variables to TLA+ specifications, ensuring
that the augmented specification is equivalent to the original one. The rules
are explained with toy examples, and they are used to verify the correctness of
a simplified version of a snapshot algorithm due to Afek et al.