Comment by callbacker

One of the authors here. Thanks for pointing that out. TLA+ spec can be found here -- https://github.com/bloomberg/blazingmq/tree/main/etc/tlaplus.