Towards Automating Blockchain Consensus Verification with IsabeLLM

TL;DR

The paper addresses the challenge of verifying blockchain consensus protocols, focusing on PoW, where correctness is critical under adversarial conditions. It introduces IsabeLLM, a general interface that bridges Isabelle with an LLM to automate formal proofs. Using IsabeLLM, the authors formalise Bitcoin's PoW via an $n$-ary-tree consensus underpinning the Bitcoin Backbone Protocol and prove consensus under majority honesty with the $k$-block common-prefix property. Results show correct proofs for non-trivial lemmas, but highlight practical bottlenecks such as API latency, LLM hallucinations, and the need for iterative refinement; future work includes parallel proof trees, multi-LLM strategies, and integration with blockchain verification frameworks.

Abstract

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.

Figures (3)

• Figure 1: Consensus theorem in Isabelle
• Figure 2: IsabeLLM Architecture.
• Figure 3: IsabeLLM example workflow.