# Towards Automating Blockchain Consensus Verification with IsabeLLM

arXiv: https://arxiv.org/abs/2601.07654 · HTML: https://mlsanity.com/paper/2601.07654/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 58 references that are in the map.
- First posted on arXiv 12 Jan 2026.

## Builds on (most cited first, 13 of 13)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving](https://mlsanity.com/paper/2406.14408/) (2024)
- [Verifying Strong Eventual Consistency in Distributed Systems](https://mlsanity.com/paper/1707.01747/) (2017)
- [A theory of Automated Market Makers in DeFi](https://mlsanity.com/paper/2102.11350/) (2021)
- [Formalizing Automated Market Makers in the Lean 4 Theorem Prover](https://mlsanity.com/paper/2402.06064/) (2024)
- [Modelling Bitcoin in Agda](https://mlsanity.com/paper/1804.06398/) (2018)
- [Towards a Verified Model of the Algorand Consensus Protocol in Coq](https://mlsanity.com/paper/1907.05523/) (2019)
- [Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs](https://mlsanity.com/paper/2106.05987/) (2021)
- [Verification of Bitcoin Script in Agda using Weakest Preconditions for Access Control](https://mlsanity.com/paper/2203.03054/) (2022)
- [A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts](https://mlsanity.com/paper/1902.08726/) (2019)

## Built on by (most cited first, 1 of 1)

- [IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus](https://mlsanity.com/paper/2606.18098/) (2026)

## Abstract (arXiv)

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.