Towards Automating Blockchain Consensus Verification with IsabeLLM

• URL: http://arxiv.org/abs/2601.07654v1
• Date: Mon, 12 Jan 2026 15:35:08 GMT
• Title: Towards Automating Blockchain Consensus Verification with IsabeLLM
• Abstract summary: 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.
• Score: 1.9336815376402718
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Consensus protocols are crucial for a blockchain system as they are what allow agreement between the system's nodes in a potentially adversarial environment. For this reason, it is paramount to ensure their correct design and implementation to prevent such adversaries from carrying out malicious behaviour. Formal verification allows us to ensure the correctness of such protocols, but requires high levels of effort and expertise to carry out and thus is often omitted in the development process. In this paper, we present IsabeLLM, a tool that integrates the proof assistant Isabelle with a Large Language Model to assist and automate proofs. 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. We use the DeepSeek R1 API for this demonstration and found that we were able to generate correct proofs for each of the non-trivial lemmas present in the verification.

Related papers

• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Vero is the first benchmark to evaluate joint implementation and proof at the repository level.<n>It contains 43 multi-module instances from real-world repositories spanning Python, Dafny, Verus, and Coq.<n>To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification.
  arXiv  Detail & Related papers  (2026-08-13T17:41:27Z)
• IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus [1.9336815376402718]
  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.
  arXiv  Detail & Related papers  (2026-06-16T16:00:14Z)
• Proof of Source of Funds: Efficient On-chain Provenance of Cryptoassets [5.222265639534245]
  We introduce Proof of Source of Funds (PoSoF), a novel cryptographic framework that shifts the burden to the user.<n>PoSoF provides verifiable cryptographic provenance; it guarantees the legitimacy of the funds without leaking the intermediate transaction topology.<n>Our benchmarks demonstrate that fully private, proactive compliance is highly practical.
  arXiv  Detail & Related papers  (2026-06-08T21:07:02Z)
• Temporal Motif-aware Graph Test-time Adaptation for OOD Blockchain Anomaly Detection [55.18577006122169]
  We propose a novel framework termed textbfTEmporal textbfMotif-aware textbfGraph textbfTest-textbfTime textbfAdaptation (textbfTEMG-TTA)<n>First, we comprehensively capture the 3-node temporal motif distribution of each active address using an efficient computational mechanism.<n>Second, we design a simple yet effective test-time adaptation strategy to facilitate the sharing of common patterns between training and testing graphs.
  arXiv  Detail & Related papers  (2026-05-28T07:43:20Z)
• 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)
• SEDULity: A Proof-of-Learning Framework for Distributed and Secure Blockchains with Efficient Useful Work [41.41842611951311]
  We name the framework SEDULity, which stands for a Secure, Efficient, Distributed, and Useful Learning-based blockchain system.<n>We show that our framework is distributed, secure, and efficiently trains ML models.<n>We further demonstrate that the proposed PoL framework can be extended to other types of useful work and design an incentive mechanism to incentivize task verification.
  arXiv  Detail & Related papers  (2025-12-15T18:55:20Z)
• Proof of Trusted Execution: A Consensus Paradigm for Deterministic Blockchain Finality [0.391985484065646]
  We propose Proof of Trusted Execution (PoTE), a consensus paradigm where agreement emerges from verifiable execution rather than replicated re-execution.<n>Because the execution is deterministic and the proposer is uniquely derived from public randomness, PoTE avoids forks, eliminates slot.time bottlenecks, and commits blocks in a single round of verification.
  arXiv  Detail & Related papers  (2025-12-10T08:04:38Z)
• Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
  Despite Etherscan's 78,047,845 smart contracts deployed on (as of May 26, 2025), a mere 767,520 ( 1%) are open source.<n>This opacity necessitates the automated semantic analysis of on-chain smart contract bytecode.<n>We introduce a pioneering decompilation pipeline that transforms bytecode into human-readable and semantically faithful Solidity code.
  arXiv  Detail & Related papers  (2025-06-24T13:42:59Z)
• Think Before You Accept: Semantic Reflective Verification for Faster Speculative Decoding [48.52389201779425]
  Speculative decoding accelerates inference by generating multiple draft tokens using a lightweight model and verifying them in parallel.<n>Existing verification methods rely heavily on distributional consistency while overlooking semantic correctness.<n>We propose Reflective Verification, a training-free and semantics-aware approach that achieves a better trade-off between correctness and efficiency.
  arXiv  Detail & Related papers  (2025-05-24T10:26:27Z)
• Formal Model Guided Conformance Testing for Blockchains [1.4838910416636741]
  We present a framework that performs protocol conformance testing using a formal model of the protocol.<n>Our framework consists of two complementary components that use the components as trace generators and checkers.
  arXiv  Detail & Related papers  (2025-01-15T03:20:13Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  We introduce a benchmark to assess the ability of Large Language Models to autonomously identify vulnerabilities in new cryptographic protocols. We created a dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents.
  arXiv  Detail & Related papers  (2024-11-20T14:16:55Z)
• BlockScan: Detecting Anomalies in Blockchain Transactions [16.73896087813861]
  BlockScan is a customized Transformer for anomaly detection in blockchain transactions.<n>This work sets a new benchmark for applying Transformer-based approaches in blockchain data analysis.
  arXiv  Detail & Related papers  (2024-10-05T05:11:34Z)
• Scalable Zero-Knowledge Proofs for Verifying Cryptographic Hashing in Blockchain Applications [16.72979347045808]
  Zero-knowledge proofs (ZKPs) have emerged as a promising solution to address the scalability challenges in modern blockchain systems. This study proposes a methodology for generating and verifying ZKPs to ensure the computational integrity of cryptographic hashing.
  arXiv  Detail & Related papers  (2024-07-03T21:19:01Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. Key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness.
  arXiv  Detail & Related papers  (2023-05-20T11:26:51Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)
• Post-Quantum VRF and its Applications in Future-Proof Blockchain System [13.386254282693335]
  A verifiable random function (VRF) is a powerful pseudo-random function that provides a non-interactively public verifiable proof for the correctness of its output. We propose a generic compiler to obtain the post-quantum VRF from the simple VRF solution using symmetric-key primitives. We show potential applications of a quantum-secure VRF, such as quantum-secure decentralized random beacon and lottery-based proof of stake consensus blockchain protocol.
  arXiv  Detail & Related papers  (2021-09-05T07:10: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.