Hi zk folks! I wonder if there is any possibility of including the TLA+ specifications for ZooKeeper in the upcoming release, version 3.9.0. The proposal to provide TLA+ specifications for ZooKeeper was raised in ZOOKEEPER-3615 [1], and addressed via pull request #1690 on github [2]. Formal specifications can serve as precise documentation of the Zab design and implementation, and can help eliminate any ambiguities in the informal protocol description, which would be beneficial for ZooKeeper learners and developers. Popular consensus protocols like Paxos and Raft also provide their TLA+ specifications [3] [4] [5]. In the pull request [2], the specifications for Zab and ZooKeeper were warmly discussed and accordingly improved, and their quality has been reviewed and verified. Moreover, we have utilized the specifications to reproduce and identify several deep bugs in ZooKeeper. In summary, I believe it would be a great idea to merge the pull request and include the TLA+ specifications for ZooKeeper in the new version. Best regards, Sirius Links: [1] https://issues.apache.org/jira/browse/ZOOKEEPER-3615 [2] https://github.com/apache/zookeeper/pull/1690 [3] https://github.com/tlaplus/Examples/tree/master/specifications/Paxos [4] https://github.com/tlaplus/Examples/blob/master/specifications/PaxosHowToWinATuringAward/Paxos.tla [5] https://github.com/ongardie/raft.tla
