IsabeLLM: automated theorem proving applied to formally verifying consensus
File(s)
Accepted version
Author(s)
Jones, Elliot
Knottenbelt, William
Type
Journal Article
Abstract
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.
Date Acceptance
2026-06-16
Citation
Distributed Ledger Technologies: Research and Practice
ISSN
2769-6480
Publisher
Association for Computing Machinery (ACM)
Journal / Book Title
Distributed Ledger Technologies: Research and Practice
Copyright Statement
Copyright © 2026 Copyright held by the owner/author(s). Publication rights licensed to ACM. This is the author’s accepted manuscript made available under a CC-BY licence in accordance with Imperial’s Research Publications Open Access policy (www.imperial.ac.uk/oa-policy)
License URL
Publication Status
Published online
Date Publish Online
2026-06-26