We used this resource to put together a model for our distributed sessions management algorithm, heres a GitHub with Go implementation and PlusCal / TLA+ model [1]. We also wrote a more in depth article about it here [2] (with an interactive version in JS). It took a few attempts but eventually it clicked!
[1] https://github.com/endiangroup/compandauth [2] https://endian.io/articles/compandauth/