pith. sign in

arxiv: 2606.18098 · v1 · pith:OVD46N7Unew · submitted 2026-06-16 · 💻 cs.AI

IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus

Elliot Jones , William Knottenbelt This is my paper

Pith reviewed 2026-06-27 01:12 UTC · model grok-4.3

classification 💻 cs.AI
keywords automated theorem provingformal verificationconsensus protocolsbitcoinisabelleretrieval-augmented generationlarge language modelsproof of work
0
0 comments X

The pith

An enhanced IsabeLLM adds retrieval-augmented generation and error tracing to automate more of the formal verification of Bitcoin's proof-of-work consensus.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper improves IsabeLLM by implementing a retrieval-augmented generation framework, error tracing, and counterexample generation to give the large language model better context during theorem proving. It also adds compatibility with the current versions of Isabelle and Sledgehammer to increase efficiency. The authors then compare the original and updated versions of the tool by measuring how much of the formal proof for Bitcoin's Proof of Work consensus each can complete automatically. This targets the high cost and expertise barrier that has kept formal verification out of reach for most blockchain systems. The work shows how language-model assistance can be applied directly to an existing interactive theorem prover to reduce manual steps in consensus verification.

Core claim

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.

What carries the argument

The retrieval-augmented generation framework with error tracing and counterexample generation inside IsabeLLM, which supplies additional context to the language model while it interacts with Isabelle.

If this is right

  • A larger share of the Bitcoin proof-of-work consensus verification can be completed by the automated system rather than by hand.
  • Formal verification of consensus protocols requires less specialized expertise and effort.
  • The same augmented approach can be applied to other blockchain consensus mechanisms that have been formalized in Isabelle.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same retrieval and tracing additions could be ported to other interactive provers that already support language-model tactics.
  • If the measured gain holds, the method offers a practical route to verifying the security properties of deployed blockchain networks rather than only toy models.
  • Counterexample generation inside the loop may surface concrete attack scenarios that manual inspection would miss.

Load-bearing premise

The added retrieval-augmented generation, error tracing, and counterexample features produce a measurable increase in the portion of the Bitcoin proof-of-work consensus that Isabelle can verify automatically.

What would settle it

A side-by-side run of both IsabeLLM versions on the same Bitcoin PoW consensus formalization that shows no increase in the fraction of the proof completed without human intervention.

Figures

Figures reproduced from arXiv: 2606.18098 by Elliot Jones, William Knottenbelt.

Figure 1
Figure 1. Figure 1: IsabeLLM Architecture. 5 IsabeLLM IsabeLLM is an interface between the Isabelle proof assistant and an LLM. It is designed for general purpose and so can be used to prove any kind of statements within Isabelle. It should be noted that if you are using bespoke imports for your theory file, then they should be given to the LLM as context for it to understand. In our models, we are only importing Isabelle’s M… view at source ↗
Figure 2
Figure 2. Figure 2: IsabeLLM example workflow. Manuscript submitted to ACM [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Nitpick Example Lastly, we implemented an error trace that is added context to the LLM. In the previous paper we noted the LLM would often override changes we made between LLM calls and get stuck in a loop by repeatedly changing proof steps we have already corrected. The trace provides the exact changes that have been made since the last LLM call and highlights what should be preserved, enabling the LLM to… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper describes improvements to IsabeLLM, an Isabelle-based automated theorem prover, by adding a Retrieval-Augmented Generation (RAG) framework, error tracing, counterexample generation, and compatibility with the latest Isabelle/Sledgehammer versions. It evaluates the original and enhanced versions by their ability to complete formal verification of Bitcoin's Proof of Work consensus protocol.

Significance. If the performance gains hold under controlled conditions, the work would demonstrate a practical advance in AI-assisted formal verification for blockchain consensus protocols, extending theorem-proving tools to a high-stakes, real-world system. The explicit application to Bitcoin PoW verification and the use of Isabelle's machine-checked proofs are strengths that could make formal methods more accessible beyond safety-critical domains.

major comments (1)
  1. [Abstract] Abstract (and the performance comparison): the central claim that RAG, error tracing, and counterexample generation measurably increase the portion of the Bitcoin PoW consensus proof completed automatically is not supported by an ablation or controlled experiment. The reported comparison between IsabeLLM versions does not hold constant the underlying proof scripts, human guidance, Sledgehammer parameters, or tactic choices while toggling only the new context-augmentation components; any observed difference could therefore arise from unstated manual edits or version-specific heuristics rather than the advertised LLM enhancements.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive feedback. We address the major comment on the experimental comparison below and agree that additional controls are needed to strengthen the claims.

read point-by-point responses

  1. Referee: [Abstract] Abstract (and the performance comparison): the central claim that RAG, error tracing, and counterexample generation measurably increase the portion of the Bitcoin PoW consensus proof completed automatically is not supported by an ablation or controlled experiment. The reported comparison between IsabeLLM versions does not hold constant the underlying proof scripts, human guidance, Sledgehammer parameters, or tactic choices while toggling only the new context-augmentation components; any observed difference could therefore arise from unstated manual edits or version-specific heuristics rather than the advertised LLM enhancements.

    Authors: We agree that the current comparison between the original and enhanced IsabeLLM versions does not constitute a controlled ablation that isolates the effects of RAG, error tracing, and counterexample generation while holding proof scripts, human guidance, Sledgehammer parameters, and tactic choices fixed. The manuscript reports overall performance differences on the Bitcoin PoW verification task but does not include such an ablation study. We will revise the paper to add a controlled ablation experiment (or, if resource constraints prevent new runs, to explicitly qualify the claims and describe the experimental setup in greater detail) so that the contribution of the new components is more rigorously supported. revision: yes

Circularity Check

0 steps flagged

No circularity: tool-development report with empirical comparison, no equations or self-referential derivations

full rationale

The paper describes an engineering effort to extend IsabeLLM with RAG, error tracing, counterexample generation, and Isabelle/Sledgehammer compatibility, then reports an empirical comparison of the two versions on completing Bitcoin PoW verification steps. No derivation chain, fitted parameters, predictions, or first-principles results are present; the central claim is simply that the added features were implemented and performance was measured. External benchmarks (Isabelle proofs) are independent of any self-citation or input fitting, satisfying the self-contained criterion. No load-bearing self-citations, ansatzes, or renamings appear in the provided text.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The paper is an engineering report on tool improvements rather than a mathematical derivation, so no free parameters, domain axioms, or invented entities are extractable from the abstract.

pith-pipeline@v0.9.1-grok · 5719 in / 1130 out tokens · 29651 ms · 2026-06-27T01:12:21.172410+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

67 extracted references · 14 canonical work pages · 3 internal anchors

  1. [1]

    Alchemy. 2024. What are upgradeable smart contracts? https://docs.alchemy.com/docs/upgradeable-smart-contracts [Accessed April 2025]

    2024

  2. [2]

    Fahad Alhabardi and Anton Setzer. 2023. A simulator of Solidity-style smart contracts in the theorem prover Agda. InProceedings of the 2023 6th International Conference on Blockchain Technology and Applications (ICBTA). IEEE, Xi’an, China, 1–11

    2023

  3. [3]

    Fahad F Alhabardi, Arnold Beckmann, Bogdan Lazar, and Anton Setzer. 2022. Verification of Bitcoin Script in Agda using weakest preconditions for access control. arXiv:2203.03054 [cs.CR] Preprint

    work page arXiv 2022

  4. [4]

    Musab A Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña, and Grigore Roşu. 2019. Towards a verified model of the Algorand consensus protocol in coq. InInternational Symposium on Formal Methods (Lecture Notes in Computer Science, Vol. 11800). Springer, Cham, 362–367

    2019

  5. [5]

    Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples. 2018. Towards verifying Ethereum smart contract bytecode in Isabelle/HOL. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP). ACM, New York, NY, USA, 66–77

    2018

  6. [6]

    2024.Model Context Protocol (MCP)

    Anthropic. 2024.Model Context Protocol (MCP). https://modelcontextprotocol.io Accessed: April 2026

    2024

  7. [7]

    Massimo Bartoletti, James Hsin-yu Chiang, and Alberto Lluch Lafuente. 2021. Towards a theory of decentralized finance. InFinancial Cryptography and Data Security Workshops (FC 2021). Springer, Berlin, Heidelberg, 227–232

    2021

  8. [8]

    Massimo Bartoletti, James Hsin-yu Chiang, and Alberto Lluch-Lafuente. 2022. A theory of automated market makers in DeFi.Logical Methods in Computer Science18, 4 (2022), 12:1–12:35

    2022

  9. [9]

    Massimo Bartoletti and Roberto Zunino. 2023. A theoretical basis for blockchain extractable value. arXiv:2302.02154 [cs.CR] Preprint

    work page arXiv 2023

  10. [10]

    Jasmin Christian Blanchette and Tobias Nipkow. 2010. Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. InInteractive Theorem Proving (ITP) (Lecture Notes in Computer Science, Vol. 6172). Springer, Berlin, Heidelberg, 131–146

    2010

  11. [11]

    Blockchain.com. 2025. BTC Total Number of Transactions. https://www.blockchain.com/explorer/charts/n-transactions-total [Accessed April 2025]

    2025

  12. [12]

    Tabea Bordis, Tobias Runge, Alexander Kittelmann, and Ina Schaefer. 2023. Correctness-by-Construction: An Overview of the CorC Ecosystem.Ada Letters42, 2 (2023), 75–78

    2023

  13. [13]

    Certora. 2024. Certora Prover. https://www.certora.com/prover [Accessed April 2025]

    2024

  14. [14]

    Chainalysis. 2023. The $80 Million Qubit Hack Likely the Work of North Korea-linked Cybercriminals. https://www.chainalysis.com/blog/qubit- hack-north-korea/ [Accessed April 2025]

    2023

  15. [15]

    CoinBase. 2016. Ethereum Classic and the Ethereum hard fork. https://help.coinbase.com/en/coinbase/getting-started/crypto-education/eth-hard- fork [Accessed April 2025]

    2016

  16. [16]

    CoinDesk. 2019. The Vertcoin Cryptocurrency Just Got 51% Attacked – Again. https://www.coindesk.com/tech/2019/12/02/the-vertcoin- cryptocurrency-just-got-51-attacked-again [Accessed April 2025]

    2019

  17. [17]

    CoinDesk. 2020. Bad Actors Rent Hashing Power to Hit Bitcoin Gold With New 51% Attacks. https://www.coindesk.com/tech/2020/01/27/bad- actors-rent-hashing-power-to-hit-bitcoin-gold-with-new-51-attacks [Accessed April 2025]

    2020

  18. [18]

    CoinDesk. 2021. Ethereum Classic Hit by Third 51% Attack in a Month. https://www.coindesk.com/markets/2020/08/29/ethereum-classic-hit-by- third-51-attack-in-a-month [Accessed April 2025]

    2021

  19. [19]

    CoinMarketCap. 2025. BTC Market Capitalisation. https://coinmarketcap.com/currencies/bitcoin/ [Accessed April 2025]

    2025

  20. [20]

    Decrypt. 2024. BNB Chain Hits Record-High Sandwich Attacks Exposing $1.5 billion in Trades. https://decrypt.co/294648/bnb-smart-chain-blocks- hits-record-high-sandwich-attacks [Accessed April 2025]

    2024

  21. [21]

    Venmugil Elango, Nidhi Bhatia, Roger Waleffe, Rasoul Shafipour, Tomer Asida, Abhinav Khattar, Nave Assaf, Maximilian Golub, Joey Guman, Tiyasa Mitra, et al. 2026. LatentMoE: Toward Optimal Accuracy per FLOP and Parameter in Mixture of Experts.arXiv preprint arXiv:2601.18089(2026)

    work page arXiv 2026

  22. [22]

    Emily First, Markus Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole-Proof Generation and Repair with Large Language Models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). ACM, New York, NY, USA, 1229–1241

    2023

  23. [23]

    Simon Foster, Jonathan Julián Huerta y Munive, Mario Gleirscher, and Georg Struth. 2021. Hybrid systems verification with Isabelle/HOL: Simpler syntax, better models, faster proofs. InFormal Methods: 24th International Symposium (FM 2021) (Lecture Notes in Computer Science, Vol. 13047). Springer, Cham, 367–386. Manuscript submitted to ACM IsabeLLM: Automa...

    2021

  24. [24]

    Juan Garay, Aggelos Kiayias, and Nikos Leonardos. 2015. The bitcoin backbone protocol: Analysis and applications. InAnnual International Conference on the Theory and Applications of Cryptographic Techniques (EUROCRYPT) (Lecture Notes in Computer Science, Vol. 9057). Springer, Sofia, Bulgaria, 281–310

    2015

  25. [25]

    Fabian Gloeckle, Badr Youbi Idrissi, Baptiste Rozière, David Lopez-Paz, and Gabriel Synnaeve. 2024. Better & faster large language models via multi-token prediction.arXiv preprint arXiv:2404.19737(2024)

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  26. [26]

    Victor BF Gomes, Martin Kleppmann, Dominic P Mulligan, and Alastair R Beresford. 2017. Verifying strong eventual consistency in distributed systems.Proceedings of the ACM on Programming Languages1, OOPSLA (2017), 1–28

    2017

  27. [27]

    Gustavo Grieco, Will Song, Artur Cygan, Josselin Feist, and Alex Groce. 2020. Echidna: effective, usable, and fast fuzzing for smart contracts. In Proceedings of the 29th ACM SIGSOFT international symposium on software testing and analysis. 557–560

    2020

  28. [28]

    Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, et al. 2018. Kevm: A complete formal semantics of the Ethereum virtual machine. In2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE, Oxford, UK, 204–217

    2018

  29. [29]

    Lars Hupel and Tobias Nipkow. 2018. A verified compiler from Isabelle/HOL to CakeML. InEuropean Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 10801). Springer, Cham, 999–1026

    2018

  30. [30]

    Investopedia. 2022. Crypto Worth Over $320 Million Taken in Wormhole Hack. https://www.investopedia.com/crypto-theft-of-usd320-million- wormhole-hack-5218062 [Accessed April 2025]

    2022

  31. [31]

    Investopedia. 2024. What Are Smart Contracts on the Blockchain and How Do They Work? https://www.investopedia.com/terms/s/smart- contracts.asp [Accessed April 2025]

    2024

  32. [32]

    Isabelle/HOL. 2004. Archive of Formal Proofs. https://www.isa-afp.org/ [Accessed April 2025]

    2004

  33. [33]

    Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu

    Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. 2021. LISA: Language Models of ISAbelle Proofs. In6th Conference on Artificial Intelligence and Theorem Proving (AITP). University of Innsbruck, Innsbruck, Austria, 378–392

    2021

  34. [34]

    Elliot Jones. 2025. IsabeLLM. https://github.com/EllbellCode/IsabeLLM GitHub Repository

    2025

  35. [35]

    Elliot Jones and William Knottenbelt. 2025. Towards Automating Blockchain Consensus Verification with IsabeLLM. InInternational Conference on Blockchain Technology and Emerging Applications (Communications in Computer and Information Science, Vol. 2100). Springer, Cham, 3–18

    2025

  36. [36]

    Elliot Jones and Diego Marmsoler. 2024. Towards Mechanised Consensus in Isabelle. In5th International Workshop on Formal Methods for Blockchains (FMBC 2024) (OASIcs, Vol. 117). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 4:1–4:22

    2024

  37. [37]

    Reiss, and Dan Zecha

    Henrik Klagges, Fabian Klemm, Benjamin Merkel, Daniel Klingmann, David A. Reiss, and Dan Zecha. 2025. Assembly of Experts: Linear-time construction of the Chimera LLM variants with emergent and adaptable behaviors. arXiv:2506.14794 [cs.CL] Preprint

    work page arXiv 2025

  38. [38]

    Gerwin Klein, Thomas Sewell, and Simon Winwood. 2010. Refinement in the Formal Verification of the seL4 Microkernel. InDesign and Verification of Microprocessor Systems for High-Assurance Applications, David S. Warren (Ed.). Springer, Boston, MA, 323–339

    2010

  39. [39]

    Gabriel Leite, Filipe Arruda, Pedro Antonino, Augusto Sampaio, and AW Roscoe. 2024. Extracting formal smart-contract specifications from natural language with LLMs. InInternational Conference on Formal Aspects of Component Software (Lecture Notes in Computer Science, Vol. 14330). Springer, Cham, 109–126

    2024

  40. [40]

    Patrick Lewis et al. 2020. Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks. InAdvances in Neural Information Processing Systems (NeurIPS), Vol. 33. Curran Associates, Inc., New York, NY, USA, 9459–9474

    2020

  41. [41]

    Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C Paulson. 2020. Isarstep: a benchmark for high-level mathematical reasoning. arXiv:2006.09265 [cs.LO] Preprint

    work page arXiv 2020

  42. [42]

    Xiaohan Lin, Qingxing Cao, Yinya Huang, Haiming Wang, Jianqiao Lu, Zhengying Liu, Linqi Song, and Xiaodan Liang. 2024. FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving. arXiv:2406.14408 https://arxiv.org/abs/2406.14408 Preprint

    work page arXiv 2024

  43. [43]

    Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, and Yang Liu. 2024. Propertygpt: LLM-driven formal verification of smart contracts through retrieval-augmented property generation.arXiv preprint arXiv:2405.02580(2024)

    work page arXiv 2024

  44. [44]

    Filip Marić. 2010. Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL.Theoretical Computer Science411, 50 (2010), 4333–4356

    2010

  45. [45]

    Diego Marmsoler and Achim D Brucker. 2021. A denotational semantics of Solidity in Isabelle/HOL. InInternational Conference on Software Engineering and Formal Methods (SEFM) (Lecture Notes in Computer Science, Vol. 13085). Springer, Cham, 403–422

    2021

  46. [46]

    Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. https://bitcoin.org/bitcoin.pdf Whitepaper

    2008

  47. [47]

    Nethermind. 2024. Clear–Prove Anything About Your Solidity Smart Contracts. https://www.nethermind.io/blog/clear-prove-anything-about- your-solidity-smart-contracts [Accessed April 2025]

    2024

  48. [48]

    2002.Isabelle/HOL: A Proof Assistant for Higher-Order Logic

    Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. 2002.Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer, Berlin, Heidelberg

    2002

  49. [49]

    NVIDIA. 2026. NVIDIA-Nemotron-3-Super-120B-A12B. https://build.nvidia.com/nvidia/nemotron-3-super-120b-a12b/modelcard

    2026

  50. [50]

    OpenAI. 2025. gpt-oss-120b. https://huggingface.co/openai/gpt-oss-120b

    2025

  51. [51]

    Lawrence C Paulson. 2004. Theory Ramsey. https://isabelle.in.tum.de/website-Isabelle2021-1/dist/library/HOL/HOL-Library/Ramsey.html Isabelle/HOL Library

    2004

  52. [52]

    Lawrence C Paulson. 2015. A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle.Journal of Automated Reasoning55, 1 (2015), 1–37. Manuscript submitted to ACM 18 Elliot Jones and William Knottenbelt

    2015

  53. [53]

    Daniele Pusceddu and Massimo Bartoletti. 2024. Formalizing Automated Market Makers in the Lean 4 Theorem Prover. arXiv:2402.06064 [cs.LO] Preprint

    work page arXiv 2024

  54. [54]

    Nils Reimers and Iryna Gurevych. 2019. Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks. https://arxiv.org/abs/1908.10084

    work page internal anchor Pith review Pith/arXiv arXiv 2019

  55. [55]

    Reuters. 2021. How hackers stole $613 million in crypto tokens from Poly Network. https://www.reuters.com/technology/how-hackers-stole-613- million-crypto-tokens-poly-network-2021-08-12/ [Accessed April 2025]

    2021

  56. [56]

    Anton Setzer. 2018. Modelling bitcoin in Agda. arXiv:1804.06398 [cs.CR] Preprint

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  57. [57]

    Tianyu Sun and Wensheng Yu. 2020. A formal verification framework for security issues of blockchain smart contracts.Electronics9, 2 (2020), 255

    2020

  58. [58]

    Amitayush Thakur, Yuhuai Wu, Kellin Pelrine, Brett Holmgren, Janice Ahn, Zong Zhang, Jean-Stanislas Denain, Kevin Clark, Noah Smith, Alexandre Drouin, and Edward Grefenstette. 2023. A Language-Agent Approach to Formal Theorem-Proving. arXiv:2305.07641 [cs.AI] https: //arxiv.org/abs/2305.07641

    work page arXiv 2023

  59. [59]

    René Thiemann and Akihisa Yamada. 2016. Formalizing Jordan normal forms in Isabelle/HOL. InProceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP). ACM, New York, NY, USA, 88–99

    2016

  60. [60]

    TNG Technology Consulting GmbH. 2025. DeepSeek-TNG R1T2 Chimera. https://huggingface.co/tngtech/DeepSeek-TNG-R1T2-Chimera Model version 1.0

    2025

  61. [61]

    Dominique Unruh. 2022. scala-isabelle – a Scala library for controlling Isabelle/HOL. https://dominique-unruh.github.io/scala-isabelle/ [Accessed April 2025]

    2022

  62. [62]

    Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, et al. 2023. Lego-prover: Neural theorem proving with growing libraries. arXiv:2310.00656 [cs.LG] Preprint

    work page arXiv 2023

  63. [63]

    Hongbo Wen, Jon Stephens, Yanju Chen, Kostas Ferles, Shankara Pailoor, Kyle Charbonnet, Isil Dillig, and Yu Feng. 2024. Practical security analysis of Zero-Knowledge proof circuits. In33rd USENIX Security Symposium (USENIX Security 24). 1471–1487

    2024

  64. [64]

    Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. 2024. Deepseek-prover: Advancing theorem proving in LLMs through large-scale synthetic data. arXiv:2405.14333 [cs.CL] Preprint

    work page arXiv 2024

  65. [65]

    Kaiyu Yang and Jia Deng. 2019. Learning to prove theorems via interacting with proof assistants. InInternational Conference on Machine Learning (ICML). PMLR, Long Beach, CA, USA, 6984–6994

    2019

  66. [66]

    Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2023. LeanDojo: Theorem proving with retrieval-augmented language models.Advances in Neural Information Processing Systems36 (2023), 21573–21612

    2023

  67. [67]

    Zheng Yang, Hang Lei, and Weizhong Qian. 2020. A hybrid formal verification system in coq for ensuring the reliability and security of ethereum-based service smart contracts.IEEE Access8 (2020), 21411–21436. Appendix All relevant code for IsabeLLM can be found at: https://github.com/EllbellCode/IsabeLLM The repository includes: •Source code for IsabeLLM. ...

    2020