  Using an algorithm due to Safra for distributed termination detection as a
running example, we present the main tools for verifying specifications written
in TLA+. Examining their complementary strengths and weaknesses, we suggest a
workflow that supports different types of analysis and that can be adapted to
the desired degree of confidence.
