The goal of this workshop is to show developers of concurrent and distributed systems how to model algorithms with TLA+. Inspired by Safra's EWD998, we will design and verify a termination detection algorithm during this workshop. The focus is on applying TLA+ rather than TLA+ language itself. In other words, the workshop will follow Lamport's video course style and introduce TLA+ as we go. At the end of the workshop, attendees will have written a specification of EWD998, checked safety and liveness properties, stated fairness constraints, and encountered refinement.