Safety Verification of the Raft Leader Election Algorithm Using Athena

The Raft consensus algorithm is widely recognized for its practicality and comprehensibility in achieving consensus within distributed systems. This paper presents a comprehensive exploration of Raft, making clear key concepts and verifying critical properties. We delve into the fundamental components of Raft, encompassing leader election, log replication, and safety guarantees. Detailed explanations are shown in order to illustrate the interactions between actors during commit phases, leader selection, and other significant stages. The Athena proof system is employed to verify essential properties such as leader completeness, log consistency, and fault tolerance, ensuring the algorithm’s resilience in the face of failures. Drawing upon the Athena programming language’s actor model implementation, we simulate and validate the behavior of Raft, providing practical insights into its functionality.