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