AI 中文总结
本文通过分析20余种共识协议，建立验证方法分类体系与矩阵，指出活性验证不足等缺口，给出建议与路线图，以指导构建更严谨的共识系统。
AI 中文摘要
形式化验证对于区块链共识协议愈发关键，细微的漏洞可能导致不可逆转的经济损失与网络故障。然而，现有验证方法的文献分散于各类工具、协议族和属性类别中，阻碍了累积性进展。本文作为知识系统化论文，分析了20余种已验证的共识协议——从容错崩溃的Raft协议到容错拜占庭的HotStuff协议、基于DAG的FairDAG协议，以及权益证明的Beacon Chain协议——以建立统一的验证方法分类体系。我们引入了从非正式推理到机器检查代码证明的验证成熟度量表，并提出了将协议与已验证的安全性、活性及经济属性对应的协议-属性-方法矩阵。我们的分析揭示了持续存在的缺口：尽管活性对进展保障至关重要，但其验证仍未得到充分发展；规范与实现的脱节削弱了实际保障；可扩展性限制使验证仅能应用于小型网络。我们为工具选择和证明工程提供了实用建议，并勾勒了面向可扩展、感知经济的验证的研究路线图。本研究旨在指导研究人员和从业者构建更严谨验证的共识系统。
英文摘要
Formal verification is increasingly critical for blockchain consensus protocols, where subtle bugs can cause irreversible financial loss and network failure. Yet the literature on verification methods is fragmented across tools, protocol families, and property classes, hindering cumulative progress. This Systematization of Knowledge paper analyzes over 20 verified consensus protocols--from crash-fault-tolerant Raft to Byzantine-fault-tolerant HotStuff, DAG-based FairDAG, and proof-of-stake Beacon Chain--to establish a unified taxonomy of verification approaches. We introduce a verification maturity scale ranging from informal reasoning to machine-checked code proofs, and present a Protocol--Property--Method matrix mapping protocols to verified safety, liveness, and economic properties. Our analysis reveals persistent gaps: liveness verification remains underdeveloped despite its importance for progress guarantees; specification-implementation disconnects undermine real-world assurance; and scalability limits restrict verification to small networks. We provide practical recommendations for tool selection and proof engineering, and outline a research roadmap toward scalable, economically-aware verification. This work aims to guide both researchers and practitioners in building more rigorously verified consensus systems.
