# IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 75 references that are in the map.
- First posted on arXiv 16 Jun 2026.

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

- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks](https://mlsanity.com/paper/1908.10084/) (2019)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Better & Faster Large Language Models via Multi-token Prediction](https://mlsanity.com/paper/2404.19737/) (2024)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [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)
- [PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation](https://mlsanity.com/paper/2405.02580/) (2024)
- [FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving](https://mlsanity.com/paper/2406.14408/) (2024)
- [LatentMoE: Toward Optimal Accuracy per FLOP and Parameter in Mixture of Experts](https://mlsanity.com/paper/2601.18089/) (2026)
- [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)
- [Assembly of Experts: Linear-time construction of the Chimera LLM variants with emergent and adaptable behaviors](https://mlsanity.com/paper/2506.14794/) (2025)
- [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)
- [A Mechanised Proof of G"odel's Incompleteness Theorems using Nominal Isabelle](https://mlsanity.com/paper/2104.13792/) (2021)
- [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)
- [Towards Automating Blockchain Consensus Verification with IsabeLLM](https://mlsanity.com/paper/2601.07654/) (2026)

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

- [CAPRI: Contract-Aware Proof Repair for Isabelle](https://mlsanity.com/paper/2608.13459/) (2026)

## Abstract (arXiv)

Advances in Artificial Intelligence (AI) have led AI for Theorem Proving to become a promising means of formally verifying computer systems. Whilst formal verification is traditionally reserved for safety-critical systems due to the required amount of expertise and effort, AI can help to automate a large amount of this workload and make it far more accessible. Blockchain-based systems are becoming increasingly popular and are frequently targeted by malicious actors, often resulting in huge financial losses, highlighting the need to better verify these systems and mitigate vulnerabilities. Arguably the most important component of these systems is the consensus protocol, which allows nodes to agree on decisions in a potentially adversarial environment. In this paper, we improve upon IsabeLLM, the automated theorem proving tool in Isabelle. Namely, we implement a Retrieval-Augmented Generation framework, Error tracing and counterexample generation for improved context supplied to the Large Language Model. Compatibility with the latest version of Isabelle and Sledgehammer is also implemented for improved efficiency. We compare the performance of the two versions of IsabeLLM in their ability to complete the verification of Bitcoin's Proof of Work consensus.