Raft Distributed Consensus Protocol

Description:Formal models of the Raft distributed consensus protocol
Author(s):Hugues Evrard; Parth Bora, Pham Duc Minh, and Tim A.C. Willemse
Event(s): MARS'20, MARS'24
Paper(s): Modeling the Raft Distributed Consensus Protocol in LNT
Modelling the Raft Distributed Consensus Protocol in mCRL2


(MARS'20 paper): Consensus protocols are crucial for reliable distributed systems as they let them cope with network and server failures. For decades, most consensus protocols have been designed as variations of the seminal Paxos, yet in 2014 Raft was presented as a new, "understandable" protocol, meant to be easier to implement than the notoriously subtle Paxos family. Raft has since been used in various industrial projects, e.g. Hashicorp's Consul or etcd (used by Google's Kubernetes). The correctness of Raft is established via a manual proof, based on a TLA+ specification of the protocol. This paper reports our experience in modeling Raft in the LNT process algebra. We found a couple of issues with the original TLA+ specification of Raft, which has been corrected since. More generally, this exercise offers a great opportunity to discuss how to best use the features of the LNT formal language and the associated CADP verification toolbox to model distributed protocols, including network and server failures. (MARS'24 paper): The consensus problem is a fundamental problem in distributed systems. It involves a set of actors, or entities, that need to agree on some values or decisions. The Raft algorithm is a solution to the consensus problem that has gained widespread popularity as an easy-to-understand and implement alternative to Lamport's Paxos algorithm. In this paper we discuss a formalisation of the Raft algorithm and its associated correctness properties in the mCRL2 specification language.


    1. Download Model
    2. Browse Model
    3. tool(s): LNT (CADP)
    1. Download Model
    2. Browse Model
    3. tool(s): mCRL2
Creative Commons License    This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.