Advances in Artificial Intelligence (AI) have made AI for Theorem Proving a promising means of formally verifying computer systems. While formal verification is traditionally reserved for safety-critical systems due to the expertise and effort required, AI can help automate much of this workload, making it far more accessible.
Blockchain-based systems are increasingly popular and often targeted by malicious actors, leading to significant financial losses. This highlights the need for better verification to mitigate vulnerabilities. The consensus protocol is arguably the most important component of these systems, allowing nodes to agree on decisions in a potentially adversarial environment.
In this paper, we improve upon IsabeLLM, the automated theorem proving tool in Isabelle. 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 enhanced efficiency. We compare the performance of the two versions of IsabeLLM in their ability to verify Bitcoin's Proof of Work consensus.
Blogger's Review: This paper highlights the potential of AI in formal verification, particularly in the blockchain domain. The introduction of automated tools can significantly reduce verification costs and enhance efficiency, making it a noteworthy area for future exploration and application.