Towards Automating Blockchain Consensus Verification with IsabeLLM

TL;DR

This paper introduces IsabeLLM, a tool combining Isabelle proof assistant and large language models to automate and assist in verifying blockchain consensus protocols, demonstrated on Bitcoin's Proof of Work.

Contribution

It presents a novel integration of LLMs with formal proof assistants to automate blockchain protocol verification, reducing effort and expertise needed.

Findings

Successfully verified Bitcoin's Proof of Work protocol

Generated correct proofs for complex lemmas

Demonstrated effectiveness of LLM-assisted formal verification

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.