Our proof requires the following properties of GCDs, which for simplicity we just assume:

At any point in a TLA+ proof, there is a current obligation that
is to be proved. The obligation contains
a context of
known facts, definitions,
and declarations, and a goal.
The obligation claims that the goal is logically entailed by the
context. Some of the facts and definitions in the context are
marked as usable for
reasoning, while the remaining facts and definitions
are hidden. That obligation
is then sent to a backend
(Zenon,
Isabelle,
SMT solvers – see the tactics
section) that tries to prove it. The smaller the context is,
the faster those backends are. Hence TLAPS tries to keep that
context as small as possible. For example,
the axioms about GCD stated above are not
directly usable by the backends: they
are known
but not usable. As we have
seen in the simple proof
section, you have to explicitly

Let us get back to our example. Now that
we have proved that the initial state satisfies the invariant, let
us prove that this invariant is preserved by the next-state
relation

Let us first simplify the goal to be proved by using
a

This step asserts that it is sufficient to
prove

We'll need the definitions of

The general form of a

USE e_{1}, …,e_{m}DEFd_{1}, …,d_{n}

which asserts that the definitions *d*_{1},
… *d*_{n} are to be made usable, and the
facts *e*_{1}, …, *e*_{m} are
to be checked and then added to the context as usable. When checking
these facts, all other known facts are temporarily considered to be
usable, so it is possible to say

To prove the theorem

*step names*
(the *level*, which is 1. The proof itself consists of
four claims named by these step names (plus the two first unnamed
steps); the first three are unjustified, while the last is
justified by the cited
facts

After having asked TLAPS to prove the theorem,
the

First, the proofs of
the

Let us now prove step

Let us now prove
step

The proof of the

Then theorem

Now we have

First we prove that a stuttering step (i.e. a step that leaves
all variables unchanged) keeps the invariant unchanged. This is
proved simply by checking that the definition
of

Then we can prove that any process that follows the specification
must keep

Unfortunately, that doesn't work:

Indeed, none of the default back-end provers (SMT, Zenon, and
Isabelle) can deal with temporal logic. But TLAPS includes an
interface to a propositional temporal logic prover (LS4), which
can be invoked by adding `TLAPS.tla`

standard module, we have to explicitly extend the TLAPS module:

Then we can use the

Finally we prove that, at any point in time, our invariant entails the correctness of the result, then use that to prove the main theorem:

And this concludes the proof of correctness of Euclid's algorithm.

This is the whole file, with the specification and proofs: