On: BlazingMQ: High-performance open source message qu...

[fizwhiz]

FWIW they mention this at the bottom of their document

> Just like BlazingMQ’s other subsystems, its leader election implementation (and general replicated state machinery) is tested with unit and integration tests. In addition, we periodically run chaos testing on BlazingMQ using our Jepsen chaos testing suite, which we will be publishing soon as open source. We have also tested our implementation with a TLA+ specification for BlazingMQ’s elector state machine.

[callbacker → fizwhiz]

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 → callbacker]

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

[peheje → amelius]

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

[callbacker → peheje]

Correct