TLA+ formalization of a distributed termination-detection algorithm, including a proof checked with Apalache. See the repository by Giuliano Losa.