Apologies! I was only blindly responding to the parent comment... FWIW the phrase seems to come from here: https://bloomberg.github.io/blazingmq/docs/architect

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/election_rsm/#the-leader-election-algorithm-in-blazingmq 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 https://github.com/bloomberg/blazingmq/tree/main/etc/tlaplus