Formal Specification and Model Checking of Raft Log Replication in Maude
Takanori Ishibashi, Kazuhiro Ogata · Proceedings · 2023
Raft is a popular distributed consensus protocol and is used to build highly available and strongly consistent services in the industry.Using Maude, we formally specify the log replication in Raft and conduct model checking to check whether the protocol enjoys the Log Matching Property and the State Machine Safety Property.The Log Matching Property is that if two logs contain an entry with the same index and term, then the logs are identical in all entries up through the given index.The State Machine Safety Property is that if any two servers have applied two entries to their state machines at a same index, the two entries must be always the same.Our model checking experiments show that the protocol enjoys the properties under the condition that we limit the length of the server's log and the number of servers.