The Tortoise and the Hare in TLA+ An implementation of Robert Floyd's cycle detection algorithm, in PlusCal. For details, see this blog post.