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.

翻译：共识协议对于区块链系统至关重要，因为它们使得系统节点在潜在敌对环境中能够达成一致。因此，确保其设计与实现的正确性以防止恶意行为至关重要。形式化验证能够确保此类协议的正确性，但执行过程需要高度的努力与专业知识，因此在开发过程中常被忽略。本文提出IsabeLLM，一种将证明辅助工具Isabelle与大型语言模型集成以辅助和自动化证明的工具。我们通过使用IsabeLLM开发比特币工作量证明共识协议的新颖模型并验证其正确性，展示了该工具的有效性。本次演示使用了DeepSeek R1 API，并发现我们能够为验证中存在的每个非平凡引理生成正确的证明。