We illustrate the use of the TLA+ tool set, including the explicit-state model checker TLC, the symbolic model checker Apalache, and the proof assistant TLAPS, for verifying a distributed termination detection algorithm. This experiment demonstrates the complementarity of the different verification tools, applicable to the same specification.
(Joint work with Igor Konnov and Markus Kuppe)