IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus

• URL: http://arxiv.org/abs/2606.18098v1
• Date: Tue, 16 Jun 2026 16:00:14 GMT
• Title: IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus
• Abstract summary: We improve upon IsabeLLM, the automated proving tool in Isabelle.<n>We implement a Retrieval-Augmented Generation framework, Error tracing and counterexample generation.<n>We compare the performance of the two versions of IsabeLLM in their ability to complete the verification of Bitcoin's Proof of Work consensus.
• Score: 1.9336815376402718
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Traccia: An OpenTelemetry-Based Governance Platform for AI Systems [0.7919969809015938]
  The rapid development of Large Language Models (LLMs) and Artificial Intelligent (AI) powered autonomous agents has fundamentally changed the existing forms of software governance.<n>Current solutions fail to protect unbound state space agentic architecture from serious threats such as alignment, security concerns, and unauthorized deployment of shadow AI systems.<n>A solution is proposed for overcoming the discussed challenges in form of a coherent multi-level AI governance stack Traccia built on the top of OpenTelemetry infrastructure platform.
  arXiv  Detail & Related papers  (2026-07-15T19:14:21Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  We introduce VASO, a framework for verification-guided self-evolution of robot skill contracts.<n>VASO verifies logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications.<n>On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples.
  arXiv  Detail & Related papers  (2026-06-03T20:02:35Z)
• Provably Secure Agent Guardrail [89.79561918065122]
  Existing defense architectures rely on empirical semantic guardrails and probabilistic large model adjudicators.<n>This paper proposes a new security paradigm for agents based on the fundamental limitations of logical reasoning.
  arXiv  Detail & Related papers  (2026-05-28T02:12:41Z)
• Trustworthy AI Suffers from Invariance Conflicts and Causality is The Solution [80.98492754957466]
  Core trustworthy AI objectives, such as fairness, robustness, privacy, and explainability, are hard to achieve simultaneously.<n>This paper argues that causality is necessary to understand and balance trade-offs in performance and multiple objectives of trustworthy AI.
  arXiv  Detail & Related papers  (2026-05-04T14:26:28Z)
• Reasoning-Aware AIGC Detection via Alignment and Reinforcement [55.09684020007737]
  REVEAL is a framework that generates interpretable reasoning chains before classification.<n>It achieves state-of-the-art performance across multiple benchmarks.
  arXiv  Detail & Related papers  (2026-04-21T07:29:55Z)
• CREDIT: Certified Ownership Verification of Deep Neural Networks Against Model Extraction Attacks [54.04030169323115]
  We introduce CREDIT, a certified ownership verification against Model Extraction Attacks (MEAs)<n>We quantify the similarity between DNN models, propose a practical verification threshold, and provide rigorous theoretical guarantees for ownership verification based on this threshold.<n>We extensively evaluate our approach on several mainstream datasets across different domains and tasks, achieving state-of-the-art performance.
  arXiv  Detail & Related papers  (2026-02-23T23:36:25Z)
• Towards Automating Blockchain Consensus Verification with IsabeLLM [1.9336815376402718]
  We present IsabeLLM, a tool that integrates the proof assistant Isabelle with a Large Language Model to assist and automate proofs.<n>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.
  arXiv  Detail & Related papers  (2026-01-12T15:35:08Z)
• Agentic Program Verification [14.684859166069012]
  We present a first Large Language Models agent, AutoRocq, for conducting program verification.<n>Unlike past works, which rely on extensive training of LLMs on proof examples, our agent learns on-the-fly and improves the proof via an iterative refinement loop.<n>In this way, our proof construction involves autonomous collaboration between the proof agent and the theorem prover.
  arXiv  Detail & Related papers  (2025-11-21T15:51:48Z)
• SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems [12.181911851729614]
  We present SysMoBench, a benchmark that evaluates AI's ability to formally model large, complex systems.<n>We focus on concurrent and distributed systems, which are keystones of today's critical computing infrastructures.
  arXiv  Detail & Related papers  (2025-09-27T05:24:54Z)
• A Hashgraph-Inspired Consensus Mechanism for Reliable Multi-Model Reasoning [0.0]
  Inconsistent outputs and hallucinations from large language models (LLMs) are major obstacles to reliable AI systems.<n>This paper proposes a novel consensus mechanism, inspired by distributed ledger technology, to validate and converge these outputs.
  arXiv  Detail & Related papers  (2025-05-06T14:05:12Z)
• Networks of Networks: Complexity Class Principles Applied to Compound AI Systems Design [63.24275274981911]
  Compound AI Systems consisting of many language model inference calls are increasingly employed. In this work, we construct systems, which we call Networks of Networks (NoNs) organized around the distinction between generating a proposed answer and verifying its correctness. We introduce a verifier-based judge NoN with K generators, an instantiation of "best-of-K" or "judge-based" compound AI systems.
  arXiv  Detail & Related papers  (2024-07-23T20:40:37Z)
• Auto.gov: Learning-based Governance for Decentralized Finance (DeFi) [14.697580721893809]
  "Auto$.$gov" is a learning-based governance framework that employs a deep Qnetwork reinforcement learning (RL) strategy to perform semi-automated, data-driven parameter adjustments.<n>In tests with real-world data, Auto$.$gov outperforms the benchmark approaches by at least 14% and the static baseline model by tenfold.
  arXiv  Detail & Related papers  (2023-02-19T12:11:41Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.