Abstract:Distributed systems play an important role in the computing environment. The consensus protocol is used to guarantee the consistency between nodes. The design error in the consensus protocol might cause failure in the operation of the system and might bring catastrophic consequences to humans or the environment. Therefore, proving the correctness of the consensus protocol is very important. Formal verification can strictly prove the correctness of the target properties in the design model, which is suitable for verifying consensus protocols. However, with the scale of distributed systems increasing, it becomes more complicated to verify its correctness, which brings more challenges to the formal verification techniques. What method to use to formally verify the design of the consensus protocol and how to increase the verification scale are important research issues in the formal verification of the consensus protocol. This paper investigates the current research on the use of formal methods to verify consensus protocols, summarizes the key techniques and main methods, and proposes future research directions in this field.