用大模型辅助形式化验证区块链共识协议，提升安全性与效率。
Towards Automating Blockchain Consensus Verification with IsabeLLM
- 结合Isabelle证明助手与大语言模型自动生成证明。
- 成功验证比特币PoW协议中多个关键lemma的正确性。
- 适合安全研究者与区块链开发人员快速验证协议设计。
共识协议是区块链系统的核心，确保节点在潜在敌对环境中达成一致。为防止恶意行为，协议的设计与实现必须正确，而形式化验证是保障正确性的有效手段，但通常需要高成本和专业知识，因此常被忽略。本文提出IsabeLLM，将证明助手Isabelle与大语言模型（使用DeepSeek R1 API）集成，用于辅助和自动化证明。我们利用该工具构建了比特币工作量证明（Proof of Work）共识协议的新模型，并验证其正确性。实验表明，IsabeLLM能够生成每个非平凡lemma的正确证明，验证过程高效且可靠。
原文摘要 · Abstract (English)
Consensus protocols are crucial for a blockchain system as they are what allow agreement between the system's nodes in a potentially adversarial environment. For this reason, it is paramount to ensure their correct design and implementation to prevent such adversaries from carrying out malicious behaviour. Formal verification allows us to ensure the correctness of such protocols, but requires high levels of effort and expertise to carry out and thus is often omitted in the development process. In this paper, we present IsabeLLM, a tool that integrates the proof assistant Isabelle with a Large Language Model to assist and automate proofs. We demonstrate the effectiveness of IsabeLLM by using it to develop a novel model of Bitcoin's Proof of Work consensus protocol and verify its correctness. We use the DeepSeek R1 API for this demonstration and found that we were able to generate correct proofs for each of the non-trivial lemmas present in the verification.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。