Formalization and Verification of the Zab Protocol Using CSP

ZooKeeper Atomic Broadcast (Zab) is a high-performance atomic broadcast protocol, which is a key component of Apache ZooKeeper. By ensuring strong consistency and fault tolerance, the Zab protocol plays a crucial role in building robust and resilient distributed systems. However, the correctness and reliability of the Zab protocol have received limited attention in research. Thus, we employ Communicating Sequential Processes (CSP) to analyze and evaluate of the Zab protocol’s properties and behavior. We utilize Process Analysis Toolkit (PAT) to verify six important properties, including Deadlock Freedom, Divergence Freedom, Data Reachability, Consistency, Sequentiality and Atomicity. The verification results demonstrate that the Zab protocol provides assurance of correctness and reliability.