Comment by agentultra

Do they publish formal specifications of these distributed algorithms?

Has anyone verified the implementation?

Zookeeper is at least based on Paxos which has a TLA+ model one can check.