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.

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.

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

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

Correct

> "deliberately avoids any formal specification or proof"

> how is this possibly a selling point?

Context.

In an overview doc? The informal version is accessible to more audiences.

As the canonical design doc for the system? It's certainly not.

Apologies! I was only blindly responding to the parent comment...

FWIW the phrase seems to come from here: https://bloomberg.github.io/blazingmq/docs/architecture/elec...

The full sentence reads:

"This section explains the leader election algorithm at a high level. It is by no means exhaustive and deliberately avoids any formal specification or proof."

Which makes a lot more sense.

And as noted in a sibling comment there is actually a TLA+ spec for the leader election: https://github.com/bloomberg/blazingmq/tree/main/etc/tlaplus