IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus

The paper introduces an enhanced version of IsabeLLM, an automated theorem proving tool within the Isabelle framework, which now incorporates a Retrieval-Augmented Generation (RAG) framework along with error tracing and counterexample generation to improve context for the Large Language Model. The updated IsabeLLM demonstrates improved efficiency and compatibility with the latest Isabelle and Sledgehammer versions, specifically in verifying Bitcoin's Proof of Work consensus protocol. This advancement is significant for practitioners as it automates formal verification processes, making them more accessible and effective in securing blockchain systems against vulnerabilities.