[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.

[amelius]

How is this "deliberately avoiding any formal specification or proof"?

[peheje]

I think they are referring to the specific section below the notice.

[callbacker]

Correct