About the Apalache Success Stories category

You have used Apalache to check a non-trivial TLA+ specification? Tell us about it!