Towards Automating Blockchain Consensus Verification with IsabeLLM
This work addresses the problem of reducing the high effort and expertise required for formal verification in blockchain development, offering a tool that automates proof generation, though it is incremental as it builds on existing proof assistants and LLMs.
The paper tackles the challenge of automating formal verification for blockchain consensus protocols by introducing IsabeLLM, a tool that integrates Isabelle with a Large Language Model, and demonstrates its effectiveness by successfully generating correct proofs for all non-trivial lemmas in verifying Bitcoin's Proof of Work protocol.
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.