Survey of Consensus Protocol’s Formal Verification

Abstract As blockchain technology is increasingly being applied to various aspects of actual production, higher requirements are being placed on its stability and correctness. As the core logical structure of the blockchain system, the consensus protocol bears the pressure of coordinating, exchanging, and processing information among all parties in the system, and it also requires further improvement. Currently, the improvement and development of the consensus protocol have reached a level that can effectively cope with the pressures and requirements of the current situation. However, with the development of computing technology, the computing power of all parties will continue to improve, and the threat to the consensus protocol will also increase simultaneously. Traditional simulation verification methods may no longer be able to meet existing requirements. More scientific verification methods should be employed when designing protocols to ensure accuracy and reliability. Additionally, a unified induction of the current verification level for each protocol is necessary to facilitate a more comprehensive analysis of future research ideas. This paper begins with an overview of consensus protocols, gathering and summarizing extensive research on the use of formal methods to verify protocol formulas. It analyzes the common properties of these verification protocols, along with their definitions and formal expressions. The paper then examines the methods and tools commonly employed for formal verification, discussing the characteristics of each approach, current research trends, and the challenges that remain to be addressed. Through the analysis of specific case studies, we outline the historical context and current achievements in this area, providing valuable references for future research.