Neural Theorem Proving for Verification Conditions: A Real-World Benchmark
Authors: Qiyuan Xu
Xiaokun Luan
Renxi Wang
Joshua Ong Jun Leang
Peixin Wang
Haonan Li
Wenda Li
Conrad Watt
Venue: ICLR 2026 Poster (2026)
Keywords: Neural Theorem Proving
Program Verification
AI for Verification
Automated Theorem Proving
Lean
Isabelle
Rocq
Primary area: datasets and benchmarks
TL;DR: We present the first multilingual benchmark for neural theorem proving of verification conditions --- the core proving task of program verification --- from both concise algorithms and industrial projects like Linux and Contiki-OS.

Abstract: Theorem proving is fundamental to program verification, where the automated proof of Verification Conditions (VCs) remains a primary bottleneck. Real-world program verification frequently encounters hard VCs that existing Automated Theorem Provers cannot prove, leading to a critical need for extensive manual proofs that burden practical application. While Neural Theorem Proving (NTP) has achieved significant success in mathematical competitions, demonstrating the potential of machine learning approaches to formal reasoning, its application to program verification—particularly VC proving—remains largely unexplored. 
Despite existing work on annotation synthesis and verification-related theorem proving, no benchmark has specifically targeted this fundamental bottleneck: automated VC proving.
This work introduces Neural Theorem Proving for Verification Conditions (NTP4VC) and presents the first real-world multi-lingual benchmark for this task. Specifically, from real-world projects such as Linux and Contiki-OS kernel, our benchmark leverages industrial pipelines (Why3 and Frama-C) to generate semantically equivalent test cases across formal languages of Isabelle, Lean, and Rocq. We evaluate large language models (LLMs), both general-purpose and those fine-tuned for theorem proving, on NTP4VC. Results indicate that although LLMs show promise in VC proving, significant challenges remain for program verification, highlighting a large gap and opportunity for future research.

Published as a conference paper at ICLR 2026
NEURAL THEOREM PROVING FOR VERIFICATION CONDITIONS: A REAL- WORLD BENCHMARK
Qiyuan Xu Xiaokun Luan', Renxi Wang', Joshua Ong Jun Leang*6, Peixin Wang',
Haonan Li;; Wenda Li", Conrad Watt!
Peking University 4 Imperial College London $ East China Normal University
Nanyang Technological University
3 MBZUAI
6 University of Edinburgh
ABSTRACT
Theorem proving is fundamental to program verification, where the automated proof of Verification Conditions (VCs) remains primary bottleneck. Real-world program verification frequently encounters hard VCs that existing Automated Theorem Provers (ATPs) cannot prove, leading critical need for extensive manual proofs that burden practical application. While Neural Theorem Proving (NTP) has achieved significant success mathematical competitions, demonstrat- ing the potential of machine learning approaches to formal reasoning, its appli- cation to program serification-patiiclll plored. Despite existing work annotation synthesis and verification-rellee reeatte the- orem proving, no benchmark has specifically targeted this fundamental bottleneck: automated VC proving. This work introduces Neural Theorem Proving for Ver- ification Conditions (NTP4VC), presenting the first real-world multi-language benchmark for this task. From real-world projects such Linux and Contiki-OS kernel, our benchmark leverages industrial pipelines (Why3 and Frama-C) to gen- erate semantically equivalent test cases across formal languages of Isabelle, Lean, and Rocq. We evaluate large language models (LLMs). both general-purpott and those fine-tuned for theorem proving, on NTP4VC. Results indicate that although LLMs show promise in VC proving, significant challenges remain for program verification, highlighting large gap and opportunity for future research.
VC proving- largely unex-
INTRODUCTION
Program verification has been fundamental to software reliability for over half a century (Hoare, 1969). While numerous industrial program verifiers have been developed and deployed in his- tory (Cousot et al., 2005), the adoption of program verification remains limited to safety-critical domains (Rushby, 2009; Woodcock et al., 2009). A primary reason is the heavy manual effort re- quired in the theorem proving of Verification Conditions (VCs) (Barnett et al., 2006): the logical propositions that encode program correctness.
VC plays central role in the conventional workflow of program verification (Cohen et al., 2009; Leino, 2010) as shown Fig. 1: the Verification Condition Generator (VCG) component aims to generate VCs and the prover aims to prove them. Conventionally, VC proving is carried out by Automated Theorem Provers (ATPs). However, ATPs excel only at specific domains of problems, and require human intervention (e.g., manual proofs and annotations) when automatic proof attempts fail or time out. Taking the widely-used industry tool Frama-C (Baudin et al., 2021) as an example, existing ATPs' insufficient capability necessitates ~600 lines of annotations for a linked list library, nearly matching the original C code length. Consequently, due to the central role of VC proving and the inadequacy of current automated approaches, VC proving has become a key bottleneck in automated program verification.
Large language models (LLLMs) have opened the door to Neural Theorem Proving (NTP) (Minervini et al., 2018), where models generate formal proofs to conduct theorem proving. While existing NTP research has focused primarily on mathematical domains, proving competition problems (Zheng
"Corresponding Author

---

Published as a conference paper at ICLR 2026
Source Code
Program Verifier
succeeds
Certificate
Verification
Property
VCG
Prover
Conditions
fails
the program is buggy OR prover not strong enough
Annotation
The prover can be either:
conventionally. ATP
OR
Neural Theorem Proving
Z3 CVC5
proposes proof
Proof Checker (ITP)
succeeds
VC
LLM
candidates
or fails
Figure 1: The conventional and NTP-based workflow of program verification.
et al., 2022; Tsoukalas et al., 2024) and formalizing mathematics (Xin et al., 2025), theorem proving extends naturally to VC proving (Harrison et al., 2014).
This motivates our central question: can NTP automate VC proving? answer this, we intro- duce Neural Theorem Proving for Verification Conditions (NTP4VC) task that applies machine-learning-bass proof generation to conduct the theorem proving of VCs.
To evaluate this task, we construct the first benchmark for NTP4VC, whose major features are com- pared with prior works in Tab. 1. challenge of this construction is that Lean (de Moura Ullrich, 2021), mainstream language in the NTP community, has relatively fewer mature program verifi- cation frameworks built on top of and large-scale industrial verification projects using it. Despite best efforts, find sufficient native VCs available in Lean for NTP4VC benchmark.
We overcome this issue by translating the VCs generated from other industrial verification pipelines (Why3 (Filliâtre & Paskevich, 2013) and Frama-C (Baudin al., 2021)) into Lean. This approach also allows us to translate VCs to Isabelle (Paulson, 1990), Roeq (Coquand & Huet, 1988) (which already implemented), and potentially other target languages, forming the first multi-language benchmark in NTP-based program verification. More crucially, this approach further allows ex- tracting VCs from existing verification projects for industrial software, such as the Linux kemel'' scheduler (Lawall et al., 2025). library functions Efremov et al. (2018), 8), and Contiki OS's 's memory allocator (Mangano et al., 2017) and linked-list library (Blanchard al., 2018).
Unlike LLM-bbsed translation approaches that suffer from LLMs' unreliability, our translation pipeline is based on ~800 expert-written translation rules for each of the three target languages (so <33 800 in total). These rules explicitly chosen ensure semantic preservation from the origins to the translations, thereby better ensuring the quality of the benchmark cases compared to LLM-based translation approaches.
We further evaluate several existing provers and LLMs on NTP4VC. For language-specific fine- tuned provers, the best model achieves only 2.08% pass @ 1, while general-purpose LLMs achieve lower performance, with GPT--44mini-hhigh achieving 1.19% pass@1 1. These results highlight the substantial difficulty of VC proving and the need for progress in NTP and LLM reasoning.
To summarize, our contribution includes:
1. We define the task of NTP4VC ($ 1), which aims to attack the automated proving of VC, key bottleneck in program verification.
2. We propose reliably automatic method for extracting corpora from real-world verification projects ($ 3). The implementation is open-sourced.
3. We present the first real-world, multi-language benchmark for NTP4VC, with open-sourced implementation and extensive evaluation of existing provers and LLMs ($ 5).
2

---

Published as a conference paper at ICLR 2026
Table 1: Comparison between our benchmark and previous ITPP-based benchmarks for program ver- ification. VC: the proportion of VC test cases. Industrial pipeline: whether the work uses industrial program verification pipelines. Language: the proof language supported by the benchmark.
Indstrial Pipeline
Language
Benchmarks
Focus
VC
Lean
Isabelle
Rocq
Lin et al. (2024)
verificatoin-
17% < 20%
X
Thompson et al. (2025)
related lemmas
X
X
Thakur et al. (2025)
0%
X
V
X
X
programming puzzles Lean
Dougherty & Mehta (2025)
0%
X
<
X
Lohn & Welleck (2024)
0%
VCs from puzzles
Ours
100%
industrial projects
VCG
cross-prover & real benchmark
Programs
from real-world industrial projects
Frama-C
Why3 code
Isabelle
Source
Spec.
Annot.
VCG frontend
Why3
Translator
Rocq
Why3 programs for pearls of algorithms, data structures
VCG backend
Lean
Source
Spec.
Annot.
Figure 2: Our pipeline for extracting benchmark cases.
BACKGROUND
Theorem proving falls broadly into two categories: Automated Theorem Proving (ATP) and In- teractive Theorem Proving (ITP). ATP achieves full automation within specific domains of proof problems. These domains are limited, and VCs in real-world verification projects often exceed these domains, leading to proof failures and inevitable human intervention (e.g., manual proofs and an- notations) in order to complete the proofs. By contrast, ITP provide highly expressive languages that enable users to construct proofs across broad domains, capable of handling almost all program verification problems. Mainstream ITP languages include Isabelle, Roeq, and Lean.
Program verification aims to verify that a program satisfies a given property. Ideally, strong enough verifier should be able complete the verification solely given the source code and the property. In practice, however, due to limitations both VCG and VC provers, users often have provide manual proofs and annotations to guide the verifier in completing the verification. The manual effort for these proofs and annotations constitutes a huge cost burden program verification.
Why3 and Frama-C are famous program verifiers widely used in the industry. Why3 provides 1) language for both programming, annotation, and specifying functional correctness, 2) VCG, and 3) powerful ATPs. A limitation is that Why3 only verify programs written in its abstract specifi- cation language. In order to verify programs written in industrial languages, Why3 is widely used as the verification backend wwell-known toolchains which translate their input language to the Why3 specification language including Frama-C, Cameleer (Pereira & Ravara, 2021). Creusot (Denis al., 2022), and EasyCrypt (Barthe et al., 2011). Frama-C is an industrial verifier for the lan- guage. It provides a frontend to process C source code and then calls Why3 to complete the verifica- tion. The input of Frama-C is C source code with properties and annotations provided as comments, and the output is Why3 code that Why3 can continue to verify. Finally, Frama-C is widely used, having verified enormous industrial programs, such as air traffic management algorithm (Dutle et al., 2021), embedded operating system (Mangano al., 2017: Blanchard et al., 2018) 1)), cryptographic modules (Peyrard al., 2018), Linux kernel scheduler (Lawall et al., 2025), and JavaCard virtual machine (Djoudi et al., 2021).
3

---

Published as a conference paper at ICLR 2026
Why3 Source
Complication Process $3.1
De-annotated Why3 Source
Why3 VCG
AST
Constant Mapping
AST
AST of VC
Target ITP
Rewrite
Print
of VC
of VC
Lanugage
Translation Process $3.2
Figure 3: The generation process of the benchmark cases and potentially training corpora.
A RELIABLE AND AUTOMATIC METHOD FOR CORPORA GENERATION
This section presents the method we use to extract real-world VCs that consitute our benchmark. The key idea is to reuse existing industrial VCGs to extract VCs from existing verification projects, and translate these VCs into the language of the target ITPs ($ 3.1). Since the projects have all passed the verifiers' checks, the VCs are guaranteed to be provable. However, this also makes them too casy to serve as valuable benchmark cases, as they may already be within reach of existing ATPs. To produce challenging benchmark cases, we introduce novel complication process ($ 3.2) to make VCs harder while keeping them provable. The complete process is illustrated in Fig. 3.
3.1 VC EXTRACTION & RULE-BASEL TRANSLATION
Various VC languages are used in industry. such as Why3, TPTP (Sutcliffe, 2024), and SMT Lib (Barrett et al., 2010). We adopt Why3 because its logic system is Simple Typed Theory (Church, 1940), relatively high-level system that is close to and entailed by the logic of mainstream ITPs like Lean, Isabelle, and Roeq, ensuring the feasibility of the translation.
The translation process begins with given Why3 source code. It first runs Why3 VCG to gener- ate VCs and calls our customized Why3 printer to dump the VCs into an XML representation of their Abstract Syntax Trees (ASTs). These ASTs are processed by Python translation framework also written by us and finally mapped into the target ITPs'' languages. The details are provided in appendix E.
While the above process enables the basic translation from Why3 to target ITP languages, our work goes beyond this strive for idiomatic translations that closely approximate native expressions on the target ITP platforms. For this, our translation process incorporates enhancements from two aspects: First, at the syntactic level, we use printing rules map specific term structures their corresponding pretty syntax defined in the ITP, including prefix, infix annotations, and ad-hoc syntax sugars like if-then-else, match-case, and list[index]. Second, we build a rewriting system to rewrite specific combinations of terms into more idiomatic expressions. Examples include rewriting integer operations into natural number operations that are more common in ITP.
The implementation of the pipeline is made of more than 2400 mapping & rewriting rules written by human experts ITP, in total for Isabelle, Lean, and Roeq. The correctness of the rules supported by syntax checking over the translation results one hand, and cross-validation by other experts (our first, second, and last authors) on the other hand. These expert-written rules form the foundation of the translations' correctness and quality. Once this foundation is built, the entire translation process is automatic, constituting a reliably automatic method for extracting VC corpora.
3.2
COMPLICATION PROCESS: EXTRACTING CHALLENGING VCs
As mentioned at the beginning of this section, the VCs extracted from real-world projects are al- ready provable by existing ATPs, thus providing insufficient challenge for benchmark evaluation. However, these VCs are provable by the ATPs as human developers have already written sufficient annotations to make them easy for ATPs to prove, rather than from inherent ATP strength. A direct idea is erase these auxiliary annotations and restore the verification tasks to what they should ideally in fully automated program verification.
Specifically, three sorts of annotations dedicated to VC simplification: (I) assert annotation, which introduces a subgoal to ask the prover to first prove this subgoal and then use the proven subgoal as lemma in the subsequent proofs; (2) lemma annotation, which explicitly introduces global lemma so that the prover can later reference it to prove subsequent propositions; (3) annota- tion of lemma application, which explicitly instantiates (the free variables in) a lemma and advises
4

---

Published as a conference paper at ICLR 2026
the prover to use it. All these annotations can be safely erased without affecting the VC's provability (by strong enough prover) (Bobot et al., 2025; Correnson et al., 2025). In addition, they exhibit clear syntactic patterns enabling to identify and erase them. Indeed, the exact job of our compli- cation process is erasing the annotations. The results show this process effectively reduces the pass rate of Why3's strongest ATP from ~99% to 622 Why3's bundled examples.
4 NTP4VC BENCHMARK
The method discussed in $ enables effective extraction of real-world VCs from existing verification projects. By applying the method, we extract >7.5k VCs from various sources. From there, we carefully select 600 VCs to constitute benchmark, with consideration for breadth, diversity, and the balance of difficulty levels as described below.
Breadth, Diversity, and the Difficulty Level. Real-world industrial projects certainly possess high value in verifi- cation benchmark like ours, while the same time, chal- lenging algorithms and data structures are equally valu- able verification targets due their complexity. An is- sue is that conflict exists between them: challenging algorithmic content is sparse in industrial project source code. If benchmark focused solely on VCs from indus- trial projects, it would underrepresent algorithms and data structures. In order to balance the breadth of the verifica- tion scenarios involved, we divide our benchmark into two equal parts (50% vs 50%). (1) Pearls of Programs con- sists of minimal working programs that capture verifica- tion pain points, including algorithms, data structures, and well-known "hard nuts to crack", such as Binomial Heap, VerifyThis'2 24 competition, and Hillel challenge (Wayne, 2018). These programs are written in Why3's abstract specification language. (2) Real Verification: VCs
Table 2: Categories of the benchmark
Category
Number
ATP pass
pearls of programs
Algorithm
20.00%
Data Structure
73
19.18%
Calculation
19.70%
Engineering Competition
54
20.37%
19.23%
real C verification
Function
81
23.46%
Loop
81
24.69%
Memory
74
24.32%
Invalid Arg.
25.00%
Total
600
22.00%
from industrial C programs used in real-world projects, such as the memory allocator (Mangano al., 2017) and the linked-list library (Blanchard al., 2018) from the Contiki Operating System.
Fach category is further divided into sub-categories (Tab. 2), with roughly balanced numbers of cases in each sub-category to maintain diversity. The pearl of programs consists of 1) Well-known algorithms such as sorting, string operations, searching, shortest path, and graph; 2) Data struc- tures, including (balanced) trees, heaps, hash, and arrays; 3) Numerical and other calculations, such as arbitrary precision arithmetics, square root, exponentiation by squaring. and bitwise operations; 4) Engineering optimization tricks (e.g., in- in-place reversal of linked lists and N-queens by bitvector) and common engineering tasks (e.g., string padding, list element removal, space-insensitive compar- ison between strings, and the challenges by Wayne (2018);: 5) Cases from well-known verification competitions, e.g., VerifyThis (Ernst al., 2019) and VSCOMP (Klebanov al., 2011).
While the pearl of programs organized by source programs' functionality, cases in the real C verification are categorized by the properties that VCs validate: 1) Function category verifies that programs' logical behavior meets the desired functionalities from a big-picture view, assuming the absence of runtime errors; 2) Loop category verifies loop termination, and loop invariants are estab- lished and maintained; 3) Memory category rules out the runtime eтror of invalid memory access; 4) Invalid Arg. checks that arguments and operands are valid. For example, the operands of multipli- cation do not cause arithmetic overflow, and the dividend is not zero.
Beyond breadth, we design the benchmark to balance difficulty across categories. We measure diffi culty using the pass rate of Why3's strongest predefined ATP tactic, Auto juto_Level__ (AL3) (Bobot et al.). AL3 a hybrid tactic that combines sophisticated heuristics and five industrial cutting-ede ATPs, Z3 (de Moura & Bjørner, 2008), CVC4 (Barrett et al., 20.1), SPASS (Weidenbach et al., 2009), Alt-Ergo (Conchon et al., 2018), and E-prover (Schulz, 2002). such that a goal is proved once any of the ATPs proves the goal. The pass rate of AL3 then indicates the state-of-the-an of Why3 ATP over the benchmark cases, denoted as ATP pass @n in Tab. 2. A VC is deemed hard if AL3 fails to prove it, making its solution an open problem. Our design goal is to set each cat-
5

---

Published as a conference paper at ICLR 2026
Table Sources of cases in real C verilication. LoC Lines of C Code (comments are excluded).
Project
# of VCs
L.C
License
Linked List Library in Contiki OS (Blanchard et al., 2018)
78
833
BSD-3-Clatte
Memory Allocator in Contiki OS (Blanchard et al., 2018)
21
BSD-3-Clause
Selected Cases from C++ STL. (Burghardt et al., 2015)
53
3263
MIT
X.509 Purser (Ebulard et al., 2019)
9
5044
BSD-3-Clause
Linux Kernel Scheduler's SWB Routine (Lawall et al., 2025)
24
216
GPLv2
Linux Kerne Library Functions (Efremov et al., 2018)
85
3533
GPLv3
String & Stdio Library in kLIBC (Carvalho et al., 2014)
14
1220
GPLv2
Paparazzi UAV Autopilot's Math Lib (Pollien al., 2021)
16
3159
GPLv2
Total
300
17413
Table 4: Statistics of involved operations. Format: average (25th - 75th percentile)
Operations
of cases
# of operations
# of distinct oprs
Size
Depth
# #o V3
Integer Arith
578
69.5 (10 - 73.5)
5.0 (4 6)
600.0 (133 - 643)
55.8 (28 74)
11.0 (1 13)
Non-Linear Arith
118
10.7 (2 14)
(1 1)
1191 (228 1370)
80.3 (12.5 115)
15.2 (1 20)
Float Arith
48.9 (38 61)
7)
337 (209- 544)
(40.5 105.5)
0.11 (0 0)
List. Sequence
46.7 (8
411
963 (198 1161)
518 (21-69)))))))))))
18.6 23)
Set, Map, Bag
59
50.3 (10- 55)
3.8 (1 6]
904 (321.5 1134)
45.3 (28 - 55.5)
26.7 (8 40)
Tree, String, Matrix
26
61.5 (14 95)
5.0 6)
822 (201 1062)
15,9 (25.5 62)
314 (6 12)
Memory
297
29.5 (13 31)
7.9 10)
357 (129- 452)
62.3 (37 80)
5.2 (0- 6)
Custom Datatype
247
87.7 (7.5 94)
7.0 (3
10)
864 (193.5 1038.5)
61.1 (25 103)
16.3 (3 22)
All
600
295.1 1 (71 339)
24.8 (21 29)
583 (129- 632)
54.5 (27 72)
10.8 (1 12)
egory's composition to target an AL33 pass rate between 20%-25%% 25%, a level that ensures sufficient open problems for advancing NTP while still allowing effective evaluation of existing approaches.
Diversity of VC Expressions While the previous subsection measures the diversity of the source and the purpose of the VCs, this subsection discusses the arithmetic and data structure operations involved in these VCs. We follow the taxonomic methodology conventionally used in the ATP field (Barrett et al., 2010; SMT-LIB Initiative), and categorize the operations according to the notions and the data types involved in their related reasoning. As listed in Tab. 4, the categories include integer arithmetics, non-linear arithmetic, and various common data structures. Some cases may define their custom datatypes beyond those provided in the standard libraries. This is captured by the Custom datatype category. Further details about this classification are given in appendix H.
For each of the categories, we count the benchmark cases that involve at least one such operation, and report the average, 25th, and 75th percentile of: # of operations, the total number of occurrences of these operations; # of unique oprs, the number of distinct operation types in each case in each case; size, the number of atomic terms; depth, the height of the abstract syntax tree of the VCs; # o3. the number of quantifiers occurring in each case. As presented in Tab. 4, the result shows our benchmark cases exhibit a wide distribution across different data structures and arithmetic operations, and also span VCs of varying scales within each category.
Sources of the Benchmark Cases, and Their Licenses. All the VCs in the benchmark are drawn from opun-sourced verification projects. The pearls of programs come from the Gallery of Verified Programs Toccata Team (2025), released under the LGPL v2.1 license alongside Why3's source code. For real C verification, VCs are collected from multiple projects, as summarized in Tab. 3.
VC Selection Process. The 600 benchmark cases are selected from over 7.5k VCs. This subsection elaborates on the selection process. The process consists of three rounds: The first round determines the domain from which the benchmark cases will be selected; in the second round, one expert performs initial screening identify ~1.5k candidate cases; three experts then collaboratively evaluate each candidate in the final round to finalize the benchmark set of 600 cases.
Recall that cases in Pearls of Programs are sourced from the Toccata Team (2025)'s collection of 224 individual projects. In the first round, we select 100 projects from which all Pearl benchmark cases will be drawn, leaving the remaining 124 projects for potential use training data. To collect

---

Published as a conference paper at ICLR 2026
as many hard VCs as possible, we prioritize selecting projects rich in hard VCs. To measure if VC is hard, we run Why3's AL3, and is hard if and only AL3 fails to solve it in 10 minutes on a 16-core workstation. For Real C Verification, do not maintain such project-level separation, and the 8 projects are all used for benchmark cases.
In the second round, we first select all the hard VCs from the domain, totaling ~1.2 cases. Since aim for the benchmark to have a 20-25% pass rate on the ATP baseline, we correspondingly select ~530 cases from the easy VCs balance the candidate set at this stage. When selecting each easy VC, we check whether it is trivially provable (e.g.. true A true). To do this, we examine the VC's logical expression, the source program. related annotations, and the specifications to check that the property verified by the VC is meaningful and commonly encountered in program verification tasks.
In the final round, we apply the same evaluation method above assess each case and refine the can- didate set while additionally considering balanced coverage across the categories shown in Tab. 2. We also consider broad project coverage by selecting cases from different projects proportionally.
Format of the Benchmark Cases. Each benchmark case is single VC (a single proof goal) placed individually in a theory file, and each such file contains exactly one VC. Every VC originates from a verification project and thus may contain project-specific concepts (e.g., the data type of binary tree), resulting in VCs with library dependencies. Consequently, this requires benchmark participants to be able to learn new concepts on-the-fly from the verification projects' dependency libraries.
Dataset Contamination. Our benchmark generally free of data contamination concerns, despite all the source programs, properties, and annotations are public. This is because: (1) The transfor- mation from program and property source code to VCs is complex. Even LLMs were trained on the original source code, they cannot trivially generate VC-level concepts. In typical program veri- fication workflows, VCs are generated only transiently and are not persistently stored or published unless done deliberately. (2) The VCs we use are derived from Why3 source code after a complica- tion process, making most of them unprovable by existing ATPs, proof' for these VCs have never existed. (3) Even if we assume the proof details of the VCs from the original Why3 source code can leak information about the proofs of the complicated Why3 code, no leakage of the proof details is discovered despite our best efforts. This is expected, since Why3 never stores detailed proofs, but only records the ATP tools used, replaying them when proofs are needed. In fact, many ATPs do not support dumping detailed proofs at all. In summary, the risk of meaningful data contamination in our benchmark is extremely low.
Caveat: Provability of Benchmark Cases. All benchmark cases are drawn (after the complication process) from verification conditions in the projects that are formally verified. Methodologicallyy, this should guarantee the provability of all benchmark cases. However, in practice, all VCs are processed through Frama-C, Why3, and our translation pipelines. Implementation bugs in any of these components may potentially render some benchmark cases unprovable. During our selection process, checked the provability of each case to the extent possible. However, due to the inherent complexity of theorem proving, we cannot guarantee the actual provability of every case. Therefore, must include this caveat in the paper regarding the provability of benchmark cases.
5 EXPERIMENTS AND EVALUATION
To evaluate the challenges posed by NTP4VC, we assess seven models, covering both general- purpose language models such as GPT--o-mini (Achiam et al.. 2024) and specialized models like DeepSeek--Proer-- (Ren et al., 2025). We also include ITP hammers to provide a baseline for comparison, including the hammers: Sledgehammer (Böhme & Nipkow, 2010) tool in Isabelle/HOI. and Coqmermer (Czajka& & Kaliszyk, 2018) in Roeq.
Models We evaluate both proprictary models (GPT-o4-mini (Achiam et al., 2024)) and open-source models (K2-Think (Cheng et al., 2025), DeepSeek-V3.1. (DeepSeek-Al et al., 2025), Qwen3 (Yang et al., 2025), DeepSeek-Prowe Prover- V2 (Ren et al., 2025). Goedel-Proved (Lin et al., 2025), Minilang (Xu et al., 2025)). Among them, DeepSeek- Proveer-rr V2 and Goedel-Prover and specialized for theorem proving using Lean, while others are general-purpose purpose reasoning models. We use 1.0 as the default temperature, and set the maximum number of tokens 32, 000 during generation.
7

---

Published as a conference paper at ICLR 2026
Table 5: Pass rates (Pass@ Pass @4 Pass@8) of various NTP models and hammer-based auto- mated theorem provers on the NTP4VC benchmark, evaluated across Lean, Rocq, and Isabelle.
Lean
Rocq
Isabelle
Model
P@
P@4
P@8
P@
P@4
P@8
P@0
4
GPT-oo4-inii-iig
0.50
0.00
1.17
DeepSeek-V35 V3.1
0.50
1.00
1.67
0.50
2.67
3.17
1.34
4.32
6.25
Qwen3-32B
0.33
0.83
1.17
0.33
1.17
1.67
0.74
2.53
3.42
Qwen3-235B-A22B
0.67
1.00
1.00
0.83
2.17
3.33
1.19
2.08
3.13
K2-think
0.00
0.00)
0.00
0.67
0.67
0.67
0.00
0.00
0.00
Goedel-Prouee Proccer---ee--Vee Prover----ver V2-32B
0.50
1.17
2.17
1.67
2.17
3.00
Minilang
2.08
7.29
11.46
CogHammer/ Sledgehammer
5.67
18.00
Metries Our primary evaluation metric is the pass @n metric. NTP models are queried multiple times for each problem, generating multiple proof attempts. A proof attempt is considered successful if it can be verified by the corresponding ITP and does not contain any fake proofs such admi: or sorry. Since hammers are mostly deterministic, we only report their pass@) performance. GPT-o4-mini is evaluated with single attempt per problem due to its cost, while other models are evaluated with 8 attempts per problem (n = 8).
Prompts We zero-shot prompting for all models, providing only the problem statement and the necessary context such as definitions and previously proved lemmas. The full prompt structures are provided in Appendix F.
Proof Verification Our proof verification setup involves extracting the proof from the model's out- and checking it within the corresponding ITP environment. We use the Lean 4.21.0, 1.0, Roeq 8.20.1, and Isabelle 2024. To prevent excessively long runtimes, we set a timeout 10 minutes for each verification attempt. Sledgehammer in Isabelle is configured SMT solvers, including CVC4 (Barrett et al., 2011), CVC5 (Barbosa et al., 2022), 73 (de Moura & Bjørner, 2008), E (Schulz, 2002), SPASS (Weidenbach et al., 2009), Vampire (Kováes & Voronkov, 2013), veriT (Schurr et al., 2021), and Zipperosition (Vukmirović et al., 2022). CoqHammer is con- figured use all its supported ATPs, including E, Vampire, Z3, and CVC4. All proof verification performed on machine with an AMD Ryzen 9 7900X CPU and 64GB RAM.
its default ATPs and
5.1 RESULTS
The results summarized in Tab. 5 high- light the difficulty of program verifi- cation for NTP models. Across all three ITPs, our experiments demon- strate that all NTP models fail to achieve pass @8 scores above 12%. This stands in sharp contrast to their strong performance on mathematics benchmarks. For example, DeepSeek- Prover-V2 reaches 55.5% pass @ on miniF2F, and Goedel-Proved Provel--Povr------ Prover-VV-322B reaches 88.1% pass @ 32. On a more challenging baseline such as Putnam- Bench, these models obtain 7.15% and 13.09% pass rates, respectively, with various attempts. This perfor- mance gap suggests that program veri- fication requires fundamentally differ- ent reasoning capabilities than com- plex mathematical benchmarks.
Table Number of problems solved and corresponding pass rates of models and hammer-bar based provers on the NTP4VC benchmark, broken down by problem category.
NTP Models
Hammers
Category
Pass / Total
Pass Rate
Pass / Total
Pass Rate
Algorithm
2/55
3.64%
4
7.27%
Data Structure
3 3/73
4.11%
10/73
13.70%
Calculation Engineering Competition
5 66
7.58%
8 66
12.12%
5/54
9.26%
7//54
12.96%
5/52
5.77%
3/52
5.77%
Pearls of Prog.
/
5.00%
32/300
10.67%
Function
6/81
7.41%
25/
30.86%
Loop
3/81
3,70%
23.46%
Memory
2/74
2.70%
18/74
24.32%
Invalid Arg.
5/64
7.81%
20/66 64
31.25%
Real Verif.
16/
5.33%
82 / 300
27.33%
Total
34/660
5.67%
114.
19.00%
8

---

Published as a conference paper at ICLR 2026
Lenna deconpose_ Froontnndde've
removing the first element an AVL tree is correctly implemented
proof
Fix d2 res
Missing parenthesis
pre: "case of AEnoty d2
| Mode l d21 r2 h aresi. node model (seq (m1 L1)) d21 (seq (n1 r2)) Cons d2 (seq [n1 rest))
(0
(if bgt
s hgt (2) hgt (2) hgt L1)) hgt (m1 rest) []
(1 (if hgt (m1 (1) hgt (n1 r2) then hgt (nt r2) else hgt (n1 (1))) het (mi res1) 1)
(-int balanctng s hgt (m1 res1) hgt (m1 r) hgt (m1 res1) hgt (m1 r) s siin balancing
(1 (if hgt (m1 res1) hgt (m1 r) then hgt (m1 r) else hgt (m1 resi))) Shhgt (n1 res)
Redundant parenthesis
Figure 4: An Isabelle proof generated by DeepSeek-V3. V3.11 for VC in the benchmark. This proof contains syntax errors, including missing closing parenthesis and two redundant closing paren- theses. The seq returns tree's elements sequence in order; the hgt gives tree's height; balancing is the balancing factor of AVL tree. The full example is provided in Appendix G.
By comparison, hammer-basee -baed provers show stronger results on NTP4VC: Sledgehammer reaches pass rate of 18.00% outperforming all the language models. By combining Sledgehammer, Mini- lang's language model achieves 1 11.46% pass rate, outperforming all other models. These results indicate that current state-of-the-art NTP models have yet surpass the classical reasoning tech- niques in VC proving. Notably, although Minilang's 's model already incorporates Sledgehammer, it still fails to surpass Sledgehammer alone on NTP4VC. This further confirms that NTP4VC repre- sents novel domain for the model, distinct from the mathematical problems it excels at.
We also report the number of problems solved per category by NTP models and hammers in Table 6. The result confirms that hammers consistently outperform match NTP models in all categories. However, the magnitude of this outperformance is non- mon--nifomm the advantage of hammers over NTP models is substantially larger in Real C Verification tasks than in Pearls of Programming.
5.2 ERROR ANALYSIS OF NTP MODELS
To understand the limitations of current NTPs on verification tasks, our qualitative analysis of failure cases reveals three recurring themes: syntactic errors, semantic confusion, and hallucination. More details are available in Appendix G.
Syntactic Errors A primary hurdle for NTPs is generating syntactically correct terms. For instance, a proof for an AVL tree VC (see Fig. 4) failed to parse due to mismatched parentheses. Correcting these purely syntactic errors allowed the term to be successfully parsed. More than 24% of generated Isabelle proofs contain syntactic errors. This highlights a key challenge of VCs: unlike typical math problems that prioritize semantic insight, VCs are often long, deeply-nesteds machine-genen generattd for- mulas. Their structure places extreme demands on a model's ability to maintain long-range syntactic coherence.
Semantic and Pragmatic Confusion more profound failure is the model's misunderstanding of the proof paradigm itself. This is common Lean, where models produce syntactically plausible but pragmatically incorrect code, leading to type errors. For example, they often use imperative- style assignments (e.g.:: i i2) instead of declarative, tactic-based reasoning. This confusion is further evidenced by proof scripts degenerating into repetitive and meaningless tactic applications (e.g., "have hig = ho; have h17 = h2 ..."), which occurs more than 64% of Lean proofs generated by Goedel-Prover-V2--33 els like DeepSeek- Prockrr-rree-Vee V2 exhibit this behavior, suggesting they become overwhelmed by VC complexity and resort semantically inappropriate code, fundamentally misinterpreting the task.
one of the state-of-the-an NTP models. Even powerful mod-
Hallucination of Non-Existent Entities Finally, models frequently hallucinate non-existent con- stants, lemmas, or tactics. For instance, GPT-o4-mini often invokes a tactic called why3, which does not exist in Roeq, as a standalone proof for an entire VC. Similarly, many models introduce undefined constants lemmas not found in the context or standard libraries. At least 9% of proof attempts in Isabelle failed due to these undefined entities. This demonstrates failure to ground the generation process within the strict formal context provided by the prover.

---

Published as a conference paper at ICLR 2026
6 RELATED WORKS
Prior benchmarks by Mugnier al. (2025); Loughridge et al. (2025); Sun et al. (2024); Yang et al. (2024); Zhong et al. (2025) consider the synthesis of annotations: given source programs and prop- erties, the task is generate annotations that enable program verifiers to succeed. Like our work, they operate directly with industrial verifiers (e.g.. Dafny (Leino, 2010), Verus (Lattuada et al., 2023)). Besides, they tackle the end-to-end automation problem, which offers direct practical value by reducing the manual annotation burden. However, as mentioned in $ 2, an ideal verifier should not require annotations in the first place, and a stronger VC prover brings us closer to this ideal ver- ifier. In terms of automated program verification, our NTP4VC task is complementary to annotation synthesis approaches - we propose to tackle the VC proving bottleneck directly, while they ap- proach the problem indirectly through annotation generation (e.g.. generating assert annotations that decompose hard VCs into simpler subgoals such that the provers can handle). Both of them are effective ways to improve automation in program verification and can be applied orthogonally.
There are also NTP benchmarks (Lin et al., 2024; Thompson et al., 2025) discussing verification- related theorem proving, typically consisting of proof goals collected from ITP projects about program verification engines and their applications. However, much of their work focuses on aux- iliary lemmas used by program verifiers and specifications - such as those for preliminaries (e.g., arithmetic of bounded integers), programming language models (e.g.. memory models), and abstract program models (e. g., binary tree algebra) - rather than VCs. detail, no more than 17% of the test cases by Lin et al. (2024) might be VCs, and no more than 20% for Thompson et al. (2025)'s work (see appendix J for details). The gap between auxiliary lemmas and VCs is crucial because VCs are the direct dncorem-proving targets that arise from program verification workflow ($ 2), while auxiliary lemmas cannot (completely) represent the mecorem-proving tasks in program verification.
Besides, the Lean benchmarks by Thakur et al. (2025); Dougherty & Mehta (2025); Lohn & Welleck (2024) are also designed for program verification. These works suffer from a limitation - they do not follow the mainstream program verification methodologies adopted in the real-world industry. Lean is a specialized language with integrated verification capabilities, where the programming lan- guage itself serves
logical reasoning language. This enables users to write Lean programs and directly verify them using the Lean system, without requiring a separate VCG for program analysis. However, program verification tasks in the real-world industry typically have to face industrial pro- gramming languages that differ substantially from logical reasoning languages. Typical industrial programming languages feature complex constructs such as mutable references, memory models, functions with side effects, and pointer arithmetics none of which are involved in the program verification tasks examined by these benchmarks This contrast further underscores the necessity of employing industrial verification pipelines to extract VCs from real-world industrial projects for benchmark construction.
Finally, we also want to mention other NTP benchmarks involving much wider domains in theorem proving, such as the works by Yang & Deng (2019); Li et al. (2021); Lohn & Welleck (2024); Yang et al. (2023); Gauthier et al. (2021); Kaliszyk et al. (2017); Bansal et al. (2019); Huang et al. (2019); Leang et al. (2025a;b), which are also important benchmarks in NTP.
7 CONCLUSION
This work introduces Neural Theorem Proving for Verification Conditions (NTP4VC), presenting the first real-world multi-language benchmark for automated VC proving - a critical bottleneck in program verification. Alongside this benchmark. this work develops a reliable extraction method using expert-written translation rules and industrial verification pipelines (Why3 and Frama-C) -C) to extract VC corpora from real-world verification projects and generate semantically equivalent VCs across Isabelle, Lean, and Rocq. Our evaluation of 600 carefully selected VCs from industrial projects reveals the substantial difficulty of this task: the strongest neural theorem provers achieve only 2.08% pass @ 1. Our error analysis reveals that the lengthy, deeply nested structure of VCs presents fundamentally different challenges to NTP models compared to mathematics competition problems. The benchmark and the corpora extraction method establish a foundation for advancing neural approaches to program verification, with the potential to achieve significant breakthroughs in automated program verification.
10

---

Published as a conference paper at ICLR 2026
ACKNOWLEDGEMENT
Conrad Watt and Qiyuan Xu are supported by the Ministry of Education, Singapore, under its Aca- demic Research Fund Tier (NTU Tier RG18/25). Conrad Watt and Qiyuan Xu are additionally supported by an NTU Nanyang Assistant Professorship Start-Up Grant. Wenda Li is supported by the Al for Math Fund from Renaissance Philanthropy and XTX Markets. Peixin Wang is supported by the National Natural Science Foundation of China (No. 92582 108) and the CCF- CCF-Huawei Populus Grove Fund.
REPRODUCIBILITY STATEMENT
We have made comprehensive artifact to ensure the reproducibility of our results and to encourage future research. The artifact contains the complete NTP4VC benchmark, the source code for our VC extraction tool, and all scripts required replicate our experiments. It is available at:
https://gite wtw.:u/..oo///ggg/g//e///e wwwp///yww2/////e2..c.
httpss//ggthuub.ccm//gg///22333
REFERENCES
Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Ale- man, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. GPT-4 Techni- Report, 2024. URL https: htttps://arxiv.orrtt org/ /ttpo////////////aa////////aaaee /t///bb/2222/ 2303. 08774.
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. HOList:
An Environment for Machine Learning of Higher Order Logic Theorem Proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pp. 454-463. PMLR, 2019. URL http:// proceedings mlr www.mmmlr......m.mmmmmm.mmmm.mmm wwwppr/svvv h/wpaaanalll.. 9a html.
Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Ab- dairhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: Versatile and Industrial-Strennth SMT Solver. In Dana Fisman and Grigore Rosu (eds.), Tools and Algorithms for the Construction and Analysis of Systems, pp. 415-442, Cham, 2022. Springer International Publishing. ISBN
Mike Barnett, Bor- Yuh Evan Chang. Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects (FMCO), volume 4111 of Lecture Notes Computer Science, pp. 364-387. Springer, 2006. URL https: / doi. org/ 10. 1110010111011211111
Clark Barrett, Aaron Stump, Cesare Tinelli, et al. The SMT-lib Standard: Version 2.0. In Pro- ceedings of the 8th international workshop on satisfubility modulo theories (Edinburgh, UK), volume 13, pp. 14, 2010.
Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Ganesh Gopalakrishnan and Shaz Qadeer (eds.), Computer Aided Verification, pp- 171-177, Berlin, Heidelberg, 201 Springer Berlin Heidelberg. ISBN 978-3-642-2D 120-1.
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. Computer- Aided Security Proofs for the Working Cryptographer. In Advances in Cryptology CRYPTO 2011, volume 6841 of Lecture Notes in Computer Science, pp. 71-90. Springer, 2011. URL https: /oi. .or.//rgg/....
007 / 978 3 642-22792-2229
Patrick Baudin, François Bobot, David Bühler, Loic Correnson, Florent Kirchner, Nikolai Kosmatov, André Maroneze, Valentin Perrelle. Virgile Prevosto, Julien Signoles, and Nicky Williams. The dogged pursuit of bug-free free C programs: the Frama-C software analysis platform. Commun. ACM, 64(8):56-68, July 2021. ISSN 0001-0782, URL https::::// //doi wrgg//lgr//... 114.11141534455

---

Published as a conference paper at ICLR 2026
Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C. In NASA Formal Methods (NFM 2018), volume 10811 of Lecture Notes in Computer Science, pp. 37-53. Springer, 2018. URL https: http:///.....r/.......o 1007/ 978-3 3- 31 10099-77739 77935-55555 5.3.
Jasmin Christian Blanchette, Fabian Meier, Andrei Popeseu, and Dmitriy Traytel. Foundational nonuniform (Co)datatypes for higher-order logic. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pp. 1-12. IEEE 2017 8005071.
Computer Society, 2017. URL https: /ww. orgg/oor//a 10. 1109/LIC9ICSSSS wtt.://////..//III.C......
François Bobot, Chan-Chrittophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 Platform. University Paris Sariay,a CNRS, Inria, version 1.8.2 edition, September 2025. Uttptt:::// /tw::://wwwwww./ why //cg//
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and An- drei Paskevich. Basic Strategies. https://www http://wwwwww33.3w org/ http///////eeccccaaccacaa caw.ctmll........mm basic-strategles Accessed: 2026-01-26.
Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement Day. In Automated Reasoning
(IJCAR 2010), volume 6173 of Lecture Notes in Computer Science, pp. 107-121. Springer,, 2010.
URL https: / /tt////oiiio/ wwt.doo.......oooooooooooooo...e wwg.///gg/oooooooo.ooo 1007 3--88-3--------- 642--4222------
Jochen Burghardt, Jens Gerlach, and Timon Lapawezyk. ACSL by example. Technical re- port, Fraunhofer FOKUS, 2015. URL htt httptttt///pubuiiaaaaa wrwannafrr..deeer
Nuno Carvalho, Cristiano da Silva Sousa, Jorge Sousa Pinto, and Aaron Tomb. Formal Verification of kLIBC with the WP Frama-C Plug-in. In Julia M. Badger and Kristin Yvonne Rozier (eds.), NASA Formal Methods (NFM 20/4), volume 8430 of Lecture Notes in Computer Science, pp-
343-358. Springer, 2014. doi: https://doi.org/10 10. 1tt.://////0.100778---------- 10000997---319-062000
Zhoujun Cheng, Richard Fan, Shibo Hao, Taylor W. Killian, Haonan Li, Suqi Sun, Hector Ren, Alexander Moreno. Daqian Zhang. Tianjun Zhong, Yuxin Xiong, Yuanzhe Hu, Yutao Xie, Xudong Han, Yuqi Wang, Varad Pimpalkhute. Yonghao Zhuang, Aaryamonvikram Singh, Xuezhi Liang, Anze Xie, Jianshu She, Desai Fan, Chengqian Gao, Liqun Ma, Mikhail Yurochkin, John Maggs, Xuezhe Ma, Guowei He, Zhiting Hu, Zhengzhong Liu, and Eric P. Xing. K2-think: A parameter-efficient reasoning system, 2025. URL https: http://axxvvvvvv 076044 6044.
Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5(2): 56-68, 1940. URL ptltps://doi..om
2337722666700
Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. VCC: A practical system for verifying con- current C. In Theorem Proving in Higher Order Logics (TPHOLs), volume 5674 of Lecture Notes in Computer Science, pp. 43.42.55 Springer, 2009. URLpttps: //diii/////////// /tt////...//111111..// 2_..
Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, and Alain Mebsout. Alt-Ergo 2.2. In SMT Workshop: International Workshop on Satisfiability Modulo Theories, Oxford, United Kingdom, July 2018. URL https: / / innriiiia. hal scwence httphhhal1111900 01960203.
Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, 76(2-3):95-120, 1988. URL https: /doii.i../////////../ org 10. 101.1101100000000000000000000 5401 (88) 90005-2 - 3.
Loic Correnson, Pascal Cuoq, Florent Kirchner, André Maroneze, Virgile Prevosto, Armand Puc- cetti, Julien Signoles, and Boris Yakobowski. Frama-C User Manual. 2025. URL https: // //frmmacc. com/ dwwndowooooooooo wwwlllldddaaaaaaa c-user--ee---eeeee --wser--auuuuuuaaaa--e---- pdf. Corresponds to Frama-C 31.0 (Gallium), released on 2025-06-24.
Patrick Cousot, Radhia Cousot, Jerôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. The ASTREÉ Analyzer. In Mooly Sagiv (ed.), Programming Languages and Systems, pp. 21-30, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. ISBN 978-3-540- 31987-0. doi:
12

---

Published as a conference paper at ICLR 2026
Lukasz Czajka and Cezary Kaliszyk. Hammer for Coq: Automation for Dependent Type Theory. Journal of Automated Reasoning, 61(1-4):423-455 453, 2018. URL
Leonardo de Moura and Sebastian Ullrich. The Lean Theorem Prover and Program- ming Language. In Automated Deduction CADE 28, volume 12699 of Lecture Notes in Computer Science, pp. 625-635. Springer, 2021. URL https: /doi. http:/dtooo////////////../ org/ 1007/
978-3-030-79876-522
Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 73: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof (eds.), Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29- April 6, 2008, Proceedings, volume 4963 of Lecture Notes in Computer Science, pp. 337-340. Springer, 2008. URL https: /ww. org/ 10. 1007/ / 0000///7-------88--22333
DeepSeek-AI, Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Cheng- gang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, Damai Dai, Daya Guo, Dejian Yang, Deli Chen, Dongjie Ji, Erhang Li, et al. Deepseek-v3 technical report, 2025. URL https: // //arxiv.org/aaatla.ee. www.org/abb///1a0 1937.
Xavier Denis, Jacques- lacques-Henri
Henri Jourdan, and Claude Marché. Creusot: A Foundry for the Deductive Verification of Rust Programs. In Formal Methods and Software Engineering (ICFEM), volume 13478 of Lecture Notes in Computer Science, pp. 90-105. Springer, 2022. URL https:// doi oogg 10. 1007/9000 3- 0-1-031-17 172444
Adel Djoudi, Martin Hána, and Nikolai Kosmatov. Formal Verification of a JavaCard Virtual Machine with Frama-C. In Formal Methods (FM 2021), volume 13047 of Lecture Notes in Computer Science, pp. 427-444. Springer, 2021. URL https://aei.org////
978 3- 00000000000000000000000000000000 9 23.
Quinn Dougherty and Ronak Mchta. Proving the coding interview: A benchmark for formally verified code generation. In 2025 IEEE/ACM 2nd International Workshop on Large Language Models for Code (LLM4Code)) pp. 72-79. IEEE, 2025. URL httts::: /ccci org /0.19//1/99////// LIM4Code6673 37. 2025. 00014.
Aaron Dutle, Mariano Moscato, Laura Titolo, César Muñoz, Gregory Anderson, and François Bobot. Formal analysis the compact position reporting algorithm. Formal Aspects of Com- puting, 33(1):65-86 Jan 2021. ISSN 1433-299X. URL https://dci. 10.10//111000///// s0C165-00 019-0-0-00000
Arnaud Ebalard, Patricia Mouy, and Ryad Benadjila. Journey RTE-free X.509 parser. In Symposium sur la sécurité des technologies de I'information el des communications (SSTIC 2019), pp. 1-50, Rennes, France, 2019. URL https: /tw:://wwwwwwr. http://wwwsst..cccccc/ ceatiicoorr. http://ww..u..............enaaae
sssicrouo-Aatiicle--ooozeee-e nouy_benadjjy la aaalla__xxxvvvv_ee pdf. Talk on 6 June 2019; paper PDF available via the presentation page.
Denis Efremmo, Mikhail Mandrykin, and Alexey Khoroshilov, Deductive Verification of Unmodified Linux Kernel Library Functions. In Tiziana Margaria and Bernhard Steffen (eds.), Leveraging Applications of Formal Methods, Verification and Validation. Verification (ISoLA 20/8), volume 11245 of Lecture Notes in Computer Science, pp. 216-234. Springer, 2018. URL https://
/trgg/1..0 10. 1007/978 dei.0/9/10.1007/978 0777883-030-
Gidon Ernst, Marieke Huisman, Wojciech Mostowski, and Mattias Ulbrich. VerifyThis Verifica- tion Competition with a Human Factor. In Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen (eds.), Tools and Algorithums for the Construction and Analysis of Systems 25 Years of TACAS: TOOLympies, Held Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, volume 11229 Lecture Notes in Computer Science, pp. 175-195. Springer, 2019. URL https: / /ow./////... org / 10. 1007 3-000-1700------------
13

---

Published as a conference paper at ICLR 2026
Cean-Christophe Filliâtre and Andrei Paskevich. Why3 Where Programs Meet Provers. In Programming Languages and Systems (ESOP 2013), volume 7792 of Lecture Notes in Computer Science, pp. 125-128. Springer, 2013. URL https://eei.org//1..//
978-3-60 0012-37036-20 8_..
Hubert Garavel, Maurice H. ter Beek, and Jaco van de Pol. The 2020 Expert Survey on Formal Methods. In Formal Methods for Industrial Critical Systems (FMICS), volume 12327 of Lecture Notes in Computer Science, pp. 3-69. Springer, 2020. URL www.hhttps////ee http:/::///../o///////// 978 3- 030-
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. TacticToe: Learning Prove with Tactics. J. Autom. Reason., 65(2):257-286, February 2021. ISSN 0168-
7433. URL https:///////... cerei.org/100 100 10000//500111-00000555--000
John Harrison, Josef Urban, and Freek Wiedijk. History of Interactive Theorem Prov- ing. In Jörg Siekmann (ed.), Computational Logic, volume of Handbook of the His- tory of Logic, pp. 134.214. North-Holland, 2014. URL https://dci.cooo or..10..1166 B978 000-00444-500
50004-6.
C. A. R. Hoare. An axiomatic basis for computer programming. Commun, ACM, 12(10)557--580 October 1969. ISSN 0001-0782. URL https: doi. www.oog...........
wttp//..111//63233...... 000....1153332333 363259.
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: Learning En- vironment for Theorem Proving. In 7th International Conference Learning Representa- tions, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL net/ https: ptttps://openrevieet wttp://eeeeeeteeeneeeeeeeeee wwt.foormmmddillweeeoo
Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. In 5th International Conference on Learning Repre- sentations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. Open- Review.net, 2017. URL https:/ www.oeeeeeveeeeeeeeeeeeoo/e.eeee ew net. forum? id=ryuxYmvel..
Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, and Benjamin WeiB. The 1st Verified Software Competition: Experience Report. Michael J. Butler and Wolfram Schulte (eds.), FM 2011: Formal Methods 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. I. Proceedings, volume 6664 of Lecture Notes in Computer Science, pp. 168-168. Springer, 2011. 1. URL https:
doi. org/100 1t.g//1..1100000 10010007/990 / 3- --0-----3-2222----2111
Laura Kovács and Andrei Voronkov. Finst-Order Theorem Proving and Vampire. In Natasha Shary- gina and Helmut Veith (eds.), Computer Aided Verification, pp. 1-35, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. ISBN 978-3-642-39799..
Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust Programs using Linear Ghost Types. Proc. ACM Program. Lang., 7(0PPSLAI), April 2023. URL https: /doo.. org/
Julia Lawall, Keisuke Nishimura, and Jean-Pierre Lozi. Should We Balance? Towards Formal Verification of the Linux Kernel Scheduler. In Roberto Giacobazzi and Alessandra Gorla (eds.), Static Analysis (SAS 2024), volume 14995 of Lecture Notes in Computer Science, pp. 194-215. 031 74777 6 2__
Springer, 2025. URL https: doii org/oogg///.ooo /0lg/10..0 1007/97
Joshua Ong Jun Leang, Aryo Pradipta Gema, and Shay B Cohen. CoMAT: Chain of Mathemat- ically Annotated Thought Improves Mathematical Reasoning. In Christos Christodoulopoulos, Tanmoy Chakraborty, Carolyn Rose, and Violet Peng (eds.), Proceedings of the 2025 Con- ference on Empirical Methods in Natural Language Processing, pp. 20245 20274. Suzhou, China, November 2025a. Association for Computational Linguistics. ISBN 979-8-89176-333 6. doi: 10.18653/v 1tt.11.2222m222 100.025.emmlpmmaaa mani. 1024. URL https: / /aaaaaanntolooyyooeeoo wwgp:/y....g///20/ emn 1anm i in. 1024/.
14

---

Published as a conference paper at ICLR 2026
Joshua Ong Jun Leang, Giwon Hong, Wenda Li, and Shay B Cohen. Theorem Prover as Judge for Synthetic Data Generation. In Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Mo- hammad Taher Pilehvar (eds.), Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume I: Long Pupers), pp- 29941-29977, Vienna, Austria, July 2025b. Association for Computational Linguistics. ISBN 979-8-89176-251-40 doi: 10.18653/v1/ 2025.ac1-lomp 1448. URL https: /aaaaaaaanntttttoceeee / www.:llooyy.rg//2..o.o.. actp:///2....c.......c.ccae.e..a
acl-long. 1448/.
K. Rustan M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming. Artificial Intelligence, and Reasoning (LPAR), volume 6355 of Lecture Notes in Computer Science, pp. 348-370. Springer, 2010. URL https: /tte///ciiiioo orrg/.rg/// http///....r//1111000000// orrg/1.11007
978- 3- 111------2---1------11
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. IsarStep: a Benchmark for High-level Mathematical Reasoning, In International Conference on Learning Representations, 2021. URL
https: / wpwpreviewwwweee// net/ / forum?? Serummid=PPae (ud==Pj6fEuSS
Xiaohan Lin, Qingxing Cao, Yinya Huang, Haiming Wang, Jianqiao Lu, Zhengying Liu, Linqi Song, and Xiaodan Liang. FVEL: Interactive formal verification environment with large lan- guage models via theorem proving. In A. Globerson, L. Mackey, D. Belgrave, A. Fan, U. Pa- quet, J. Tomezak, and C. Zhang (eds.), Advances in Neural Information Processing Systems, volume 37, pp. 54932-54946. Curran Associates, Inc., 2024. URL https: doi..ii../// org/10. 22202/079011 1742.
Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goover-Prover: A Frontier Model for Open-Source Automated Theorem Proving, 2025. URL https::/t//attt
/250/ 07640.
Evan Lohn and Sean Welleck. miniCodeProps: Minimal Benchmark for Proving Code Properties. htttts::///ppeeeee/ http:///ppeeeeeeeeeemmmee
In Neurips Safe Generative Al Workshop 2024, 2024. URL https: forum?1d=6@Qe3vvP
Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, and Max Tegmark. DafnyBench: A Bench- mark for Formal Software Verification. Transactions on Machine Learning Research, 2025. ISSN 2835-8856. URL hwtpt:tt/////.....
atttps://opensee /opp//ppeeviieeeee/e/ee wwwp:w..eeeeee....ee. wttp::eeeeeeettteeeeeeeee wrrrmmiddyyggTVWee..
Frédéric Mangano, Simon Duquennoy, and Nikolai Kosmatov. Formal Verification of Memory Allocation Module of Contiki with Frama-C: A Case Study. In Frédéric Cuppens, Nora Cuppens, Jean-Louis Lanet, and Axel Legay (eds.), Risks and Security of Internet and Systems, pp. 114- 120, Cham, 2017. Springer International Publishing. ISBN 978-3-01..
Pasquale Minervini, Matko Bosnjak, Tim Rocktäschel, and Sebastian Riedel. Towards Neural Theo- rem Proving at Scale. CoRR, aabs/1807.00/ 2018. URL 08204.
org/ abs/ abs/1807. 18077.
Eric Mugnier, Emmanuel Anaya Gonzalez, Nadia Polikarpova, Ranjit Jhala, and Yuanyuan Zhou. Laurel: Unblocking Automated Verification with Large Language Models. Proc. ACM Program. Lang., (OOPSLA)) April 2025, URL https: //doi. org/ 0tteg//...111///1111 1145/3720499.
Lawrence C. Paulson. Isabelle: The Next 700 Theorem Provers. In Piergiorgio Odifreddi (ed.),
Logic and Computer Science, pp. 361-386. Academic Press, London, 1990.
Mário Pereira and António Ravara. Cameleer: A Deductive Verification Tool for OCaml. In Com- puter Aided Verification (CAV), volume 12760 of Lecture Notes in Computer Science, pp. 677- 689. Springer, 2021. URL https:t///// / http///oi.ioo// wrg/ http:/...1100///11 1007/00071900 978 3 -30-000--00 81688 9_31.
Alexandre Peyrard, Nikolai Kosmatov, Simon Duquennoy, Inria Lille, and Shahid Raza. Towards Formal Verification of Contiki: Analysis of the AES-CCM' Modules with Frama-C. In Pro- ceedings of the 2018 International Conference Embedded Wireless Systems and Networks, EWSN 18, pp. 264-269 International Conference on Embedded Wireless Systems and Networks (EWSN), 2018. ISBN 9780994988621.
15

---

Published as a conference paper at ICLR 2026
Baptiste Pollien, Christophe Garion, Gautier Hattenberger. Pierre Roux, and Xavier Thirioux. Ver- ifying the Mathematical Library of an UAV Autopilot with Frama-C. In Alberto Lluch La- fuente and Anastasia Mavridou (eds.), Formal Methods for Industrial Critical Systems (FMICS 2021), volume 12863 of Lecture Notes in Computer Science, pp. 167-173. Springer, 2021. URL https: //doi .rgg /10 007
Z. Z. Ren, Zhihong Shao, Junxiao Song. Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang. Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yux- uan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. DeepSeck-Prover- V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition, 2025. URL
https: /app:///axivve org/ abs/ 2504 21801.
John Rushby. Software Verification and System Assurance. In 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, pp. 3-10, 2009. URL https:// doi. 10. 1109/1101EEE SEEM. 2009.39.
Stephan Schulz. E A Brainiac Theorem Prover. Al Communications, 15(2-3):111-126, 2002.
URL https: doii wwg.oo////...oo.o...oo.ooo...... 10.0000000000
2000--2000-220 260.
Hans-Jörg Schurr, Mathias Fleury, and Martin Desharnais. Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. In André Platzer and Geoff Sutcliffe (eds.), Automated Deduction
CADE 28, pp. 450 450-467, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79876.
5. URL https:
1007/10000000 978- 3 030- 79876-5_2
SMT-LIB Initiative. SMT-LIB - logics. https:// amt - -lib-libb.. org/ wearr//ooosssshic.. shtml. Ac-
cessed: 2025-11-18.
Chuyue Sun, Ying Sheng, Oded Padon, and Clark W. Barrett. Clover: Closed-Loop Verifiable Code Generation. In Guy Avni, Mirco Giacobbe, Taylor T. Johnson, Guy Katz, Anna Lukina, Nina Narodytska, and Christian Schilling (eds.), Al Verification First International Symposium, SAIV 2024, Montreal, QC, Canada, July 22-23, 2024, Proceedings, volume 14846 of Lecture Notes in Computer Science, pp. 134-155. Springer, 2024. URL https://cci. org/ 1007/ 101-3-031--5111-0-2
Geoff Suteliffe. Stepping Stones in the TPTP World. In Christoph Benzmüller, Marijn J.H. Heule, and Renate A. Schmidt (eds.), Automated Reasoning, volume 14739, pp. 30-50. Springer Nature Switzerland, 2024. ISBN
doi: 10. 10.10077978-3-331-634888
Amitayush Thakur, Jasper Lee, George Tsoukalas, Meghana Sistla, Matthew Zhao, Stefan Zetzsche, Greg Durrett, Yisong Yue, and Swarat Chaudhuri. CLEVER: A Curated Benchmark for Formally Verified Code Generation, 2025. URL httph:tttt///ccttm wttp/v.ivvvvv////v// http://awww....gga///////00000 13938
Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Ster. Yuriy Brun, João F. Ferreira, Sorin Lerner, and Emily First. Rango: Adaptive Retrieval-Augmente Proving for Automated Software Verification. In 47th IEEE/ACM International Conference on Software Engineering, ICSE 2025, Ottaaa, ON, Canada, April 26 May 6, 2025, pp. 347-359. IEEE, 2025. URL https: /tt::///ooiie/ http://ooo.oog//////// 1109/ /t////SSE5534.. .. 2025. 00161.
Toccata Team. Gallery of verified programs. https: htaps://toccati , gi talbaaaagsess inria. en html. 2025. Joint team of Inria, CNRS and University of Pacis- Page generated on 2025-09-16 16. Accessed: 2025-09-17.
fr fr/toccata/ patpeaattggaallryiiiiiaa
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition. In A. Globerson, L. Mackey, Belgrave, A. Fan, U. Paquet, J. Tomezak, and C. Zhang (eds.), Advances in Neural Information Processing Systems, volume 37, pp. 11545-11566 Curran Associates, Inc., 2024. doi: 10.52200/079011--0366 URL https: https://prooeeeding.. neurips cc/paper Files/paper' https//pappe222///111e1 waiiaaaaaaaappp-aeeeeeeee Paper Datasets and Benchmarks.
Track.pdf.
16

---

Published as a conference paper at ICLR 2026
Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making Higher- Ondeer Superposition Work. Journal of Automated Reasoning, 66 doi:
(4):541-564, Nov 2022. ISSN 1573-0670.
URL https:
//doi. 10. 1007/000//00 / 081 7-
Hillel Wayne. The Great Theorem Prover Showdown, 2018.
URL https://wwy Blog post. Accessed: 2025-
hi hillel wayne 09-14.
Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, and Patrick Wischnewski. SPASS version 3.5. In Renate A. Schmidt (ed.), Automated Deduction CADE-22, 22nd International Conference Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, volume 5663 of Lecture Notes in Computer Science, pp. 140-145. Springer, 2009.
URL https: /tt.ioooogggoo.................. 10. 1007/ 9 3- 642-02959 2_10.
Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John Fitzgerald. Formal methods: Practice
and experience. ACM Comput. Surv. 41(4), October 2009. ISSN 0360-0300. URL https:
/ //doi. org/ 11411114111 11111...1111111145444411
Huajian Xin, Luming Li, Xiaoran Jin, Jacques Fleuriot, and Wenda Li. APE-Bench I: Towards File- level Automated Proof Engineering of Formal Math Libraries, 2025. URL https: //axxiv. org/ azg/abs/ 2504 4. 19110.
Qiyuan Xu, Renxi Wang, Peixin Wang, Haonan Li, and Conrad Watt. A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL, 2025. URL https: org/ abs/ 2507. 18885.
An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, Chujie Zheng, Dayiheng Liu, Fan Zhou, Fei Huang, Feng Hu, Hao Ge. Haoran Wei, Huan Lin, Jialong Tang, Jian Yang. Jianhong Tu, Jianwei Zhang, Jianxin Yang. Jiaxi Yang, Jing Zhou, Jingren Zhou, Junyang Lin, Kai Dang, Keqin Bao, Kexin Yang, Le Yu, Lianghao Deng, Mei Li, Mingfeng Xue, Mingze Li, Pei Zhang, Peng Wang. Qin Zhu, Rui Men, Ruize Gao, Shixuan Liu, Shuang Luo. Tianhao Li, Tianyi Tang, Wenbiao Yin, Xingzhang Ren, Xinyu Wang, Xinyu Zhang. Xuancheng Ren, Yang Fan, Yang Su, Yichang Zhang, Yinger Zhang, Yu Wan, Yuqiong Liu, Zekun Wang, Zeyu Cui, Zhenru Zhang, Zhipeng Zhou, and Zihan Qiu. Qwen3 Technical Report, 2025. URL https: attpaaaxvvvv../..a/aaaa org. wttp://.rrrabbb//////0
Chenyuan Yang. Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu K. Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang. Ziqiao Zhou, and Shan Lu. Autoverus: Automated proof generation for rust code. CoRR, 0e//2409.1308/ 2024.
URL https:tp//// /wwi. wrg/o0.gg//oooo 48540 /ARIVV 2409 13082.
Kaiyu Yang and Jia Deng. Learning to Prove Theorems via Interacting with Proof Assistants. Ka- malika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Con- ference on Machine Learning, volume 97 of Proceedings of Machine Learning Research, pp. 6984-6994. PMLR, 09-15 Jun 2019. URL https: htttp::/pproceedinggs ml mlr.ppesss/99/// yangl 9a. html.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In A. Oh. T. Naumann, A. Glober- son, K. Saenko, M. Hardt, and S. Levine (eds.), Advances Neural Information Pro- cessing Systems, volume 36. pp. 21573-21612. Curran Associates, Inc., 2023. URL ht.t.s:: httpss//ppocceednng 2ag.a6622209188773000eeeeeeeeeee pdf.
73. Arithmetic online 73 guide, 2025. URL https::/mlcroooft..gite. io/ hetiiee///retteeiiie.ee.ee Accessed: 2025-11-19.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: a cross-system benchmark for formal Olympiad-level mathematics. In The Tenth International Conference Learning
17

---

Published as a conference paper at ICLR 2026
Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. URL attps::/cppezeeveee net Doxzumidd922eqq ott.://w.........ooooooo..eeeee. FFFV..
Sicheng Zhong, Jiading Zhu, Yifang Tian, and Xujie Si. RAG-Verus, Repository-Level Program Verification with LLMs using Retrieval Augmented Generation. CoRR, abs/2502.05344, 2025.
URL httpps://ol. www.doio.ooooooooooooooooooooo 48550/ARXIV 2502 05344.
A LICENSING AND RULES OF ENGAGEMENT
A. LICENSE
As listed in Tab. 3, the source projects our benchmark cases are released under different open- source licenses, some of which are mutually incompatible (e-g., GPLv22v vs. GPLv3). However, since we not compile these code bases into a single target, we can still distribute the data under hybrid license. Accordingly, the VCs generated from these projects released under the same licenses as their original source projects. The code written by us released under the MIT License.
A.2 PROTECTION TO PREVENT DATA LEAKAGE
To prevent data leakage, if any VC from given ml w file is selected for the NTP4VC benchmark; all VCs from that mlw file should be protected and excluded from training. In contrast, other mlw files provided in our associated artifact the NTP4VC benchmark. Note that the mlw w files the Real C Verification category are generated from C projects, with each mlw w file corresponding to single C function. The identity of mlw file should be considered bound to its original C function. This means that mlw w files generated through alternative means (e.g., different compilation flags) that produce varied content should also be subject to the above protection.
protected, long as no VC from those files is included in
A.3 ACCEPTABLE IMPROVEMENTS TO THE TRANSLATION PIPELINE
The purpose of this benchmark to advance Neural Theorem Proving capabilities on proving Ver- ification Conditions. Note that NTP models built on top of specific ITP platforms are inevitably influenced by the language features and idioms of their respective platforms. The rule-based trans- lation provided in this work may not fully capture all such features and idioms, resulting in some VCs being translated into representations that are unnatural or unconventional for the target ITP platform. These should be considered as deficiencies in the translation pipeline. Therefore, to al- low for addressing these potential issues, improvements to the translation pipeline that address such unnatural unconventional representations should be considered legitimate and acceptable. To be clear, regenerating the NTP4VC benchmark using an improved translation pipeline as described above and evaluating the regenerated benchmark is likewise considered legitimate and accept- able. However, any evaluation based on a regenerated NTP4VC benchmark must explicitly report any modifications made to the translation pipeline when presenting results.
B ADDITIONAL BACKGROUND
Although VC has been introduced in 1, given its significance to our work, we provide a precise definition as follows.
Definition Given a program and a property, a Verification Condition (VC) is a mathematical proposition that, when proven true, guarantees the program satisfies the desired property.
Additionally, another aspect that remains unspecified in the main text the target property of the program verification discussed in our work. Any program verification task always considers target property. The target property considered in our benchmark is Functional Correctness, which guarantees program correctly implements its desired function - for any allowed input, the output of the program always satisfies a separately written logical specification of the program's 's behaviour (see appendix C for concrete example). Functional correctness is a verification goal widely adopted in real-world industrial practice (Garavel et al., 2020), and is also a primary capability of our toolchain components Why3 and Frama-C.
18

---

Published as a conference paper at ICLR 2026
u(), A S LA length(a) A (Vi. 0 S longtha A a[j =
exception standing for not found
let binary_eearch, (a: acray in:) (v: int: : iat
Vul.
requires y. 0 0 length(a) - aij $ abl
ensures 0.$ result length((a) A afresult] length(a) -
I(l, u) sorted(a)
raises NF - vs.
I $ u then let m m 1+ (u 11/2in
let rec -0 in ref langth
5 l
a|m] <
while 1 <= do
invariant u) variant u u-1
then (Vi, 1 SiSsism
0/1 <0
10
0 1Su-lAu ( A AZ(m+ 1,
11
let m = + div tz 1) 2 in then
12
amm
elae if < a/m]
13
assert Vi, 1..S << m +1 a[1] <'
then 0 LA -
14
15
else if [m] v then 1-
I m 1)
16
else return m
else 0 S m < length a A a(m] = 1)
17
done;
else (Vi. 0 5 fAi < lengtha - alf # v)
18
raise NF
Figure 5: (Left) A Why3 program for binary search, with the functional correctness property in cyan and annotations in orange. (Right) One of the generated VCs for its functional correctness (simplified).
C AN EXAMPLE OF VC
This section presents an example Why3 program and its VC to provide readers with concrete sense of how VCs relate to traditional mathematical theorems.
The left side of Fig. 5 presents a Why3 program for binary search. Its functional correctness property is given by the requires res, ensures, and raises clauses. requires specifies the domain of valid inputs, i.e., the given array a must be sorted. ensures and raises specify the expectation of the output
conditions that the result has to satisfy, which are, 1) the resull is valid index (i.e., between 0 and the length) such that array a's element at the index has a value of v, if no exception raises, or 2), if exception NF raises, no element in the array has value of e.
This program involves mutable references and an effectful loop, which makes direct reasoning with ITPs extremely tedious. The mature academic and industrial solution is to apply specialized pro- gram reasoning engine, like Why3's VCG, to first extract pure logical proof goals, so-called VCs.
The invariant and variant clauses annotations that help the VCG work. The invariant clause declares a loop invariant, which a formula that remains true throughout every loop iteration, and is required by the VCG process. The var ant clause declares metric which is strictly decreasing in each loop iteration. It helps to generate the VCs for ensuring loop termination.
The assert at line 13 is an annotation to the burden of VC prover. It introduces subgoal and instructs the verifier to first prove this subgoal and then use the proven subgoal as a premise (as shown in pink in Fig. 5) in the subsequent proofs. Essentially, it helps the prover decompose VCs into simpler subgoals.
The right side of Fig. 5 is one of the generated VCs for the functional correctness, mathematical statement that encodes the logic behind the program's 's behaviors. First, invariant I(l, u) represents that L, u valid boundaries of the indices of the elements of value v. Then, consider the case of I S u, where the VC verifies the loop iterations: if either a/m] < V or a afm] > the updated boundary (m + 1. or (1. m 1) must preserve the invariant, and the metric u must strictly decrease; if the program exits and returns m at line 16, the VC judges whether the return value m satisfies the expectation as stated in the ensures clause, by replacing the result variable in the ensures clause with m. At last, the last line in the VC corresponds to line 18, where the VC checks value v does not appear in array a.
Finally, we must emphasize that this iC simplified for better readability. The original VC is much more complicated (as shown in Fig. 6), where the invariant I is not defined as term, duplicated terms abound, and A-connected terms are disordered. This binary search is also one of the simplest cases in program verification, while other VCs can be much more complicated. This represents gap between competition-style mathematical theorems and VCs: the former are concise but
19

---

Published as a conference paper at ICLR 2026
( length - alt) S a(fl) let = lengtha 1nn
(0 00 < lenghha)
exception Not_found
(Vi. 0i.0g:< lengtha -
2
(Vul.
3 let binary_aearce
array int) int) int
4 requires V.J. 0. i S length(o) + oft] S ald
length
ensures Not_found A Ys. 0. length(a) - alf
result length(a) affresult]]
A (Vi. 0 S
- 15
6 raises
ifl
7 let ref - in
8 let ref length
in invariant O.I.A length(a)
then let m = 1 (u (u
9 while <= do
[0 S
< length a)
11 invariant Vi. 0 S length(a) = - variant u
[ifa/m]= <
A (m
1) in let 1 div
(0 S m + Au < length
if [mm] < v.v then
(Yi. 0 < length alj
16
else if à [m] > then
- + iiis
u
else (0 S m < lengtha)
18
else
assert a[m]
(if < a[m]
20
return
then (0 S a -
21
done;
22
raise found
(0 S l A
< length
A (44, 0 S ilength a[i] =
else (0 S m < length a) A a/m] v)
(Vi. length a/i *))
Figure 6: The original program and the original VC of Fig. 5, without simplification
quire sophisticated mathematical skills to construct paths towards proofs, whereas VCs require less intellectual creativity, but are complicated and require the prover to process enormous formulas, po- tentially extracting key information from noise to simplify the proof goals and ultimately complete the proofs.
D LIMITATION & MITIGATION
From methodological perspective, our VC extractionn method ensures all obtained VCs are provable by construction. However, implementation bugs may occur in Why3, Frama-C, or our translation pipeline, potentially rendering some VCs unprovable. To address such potential invalidation, we design the benchmark to be updatable: we will repair the VC extraction pipeline and refresh the benchmark when invalidation occurs. Since the intended semantics of VCs are grounded in the source verification projects, these updates primarily address representation issues while preserving the essential semantics of the verification problems. However, should an invalid benchmark case be irreparable in rare instances, we will climinate it from the benchmark to guarantee all remaining cases are provable.
E DETAILED EXTRACTON PIPELINE
This section provides further details on our extraction pipeline from two perspectives: approach and implementation
E. METHODOLOGY DETAILS
The translation process begins with a given Why3 source code. The process first runs Why3 VCG to generate VCs and calls our customized Why3 printer to dump the VCs into XML representation of their Abstract Syntax Trees (ASTs). These ASTs are processed by a Python translation framework also written by and finally mapped into the target ITPs' languages.
verification project typically contains multiple VCs that depend on shared Why3 theories consist- ing of lemmas, axioms, functions, and datatype definitions. These theories may further depend on
20

---

Published as a conference paper at ICLR 2026
others, forming a complex dependency graph across the project. To successfully translate the VCs, we must translate all dependent theories. Our translation process, therefore, recursively handles every theory in this dependency graph, mapping the entire verification project into the target ITPs.
In terms of structure, a Why3 theory is a sequence of declarative clements consisting of axioms, definitions of functions, and algebraic data types. All three sorts of declarations have similar coun- terparts in the target ITPs and can be mapped to them, despite two minor gaps. One regrading the non-uniform data lype (Blanchette et al., 2017), which not natively supported by Isabelle. There- fore, we circumvent all VCs involving such data types. The other gap pertains to discharging the termination check of recursive function definitions, a conventional requirement for ITPs to ensure the soundness of their logics. Some ITPs' termination checkers (Isabelle and Roeq) are not strong enough to automatically prove the well-foundedness of certain complicated recursions, even though Why3 has checked all the termination. Since the proof obligation of the termination is irrelevant to the semantics of VCs' proof obligation, we trust Why3's termination check and axiomatize this in the ITP translation in case ITP's termination checker fails.
Having the theory dependencies and theory-level declarations translated, the last work to translate the term language. Both Why3's and the ITPs' term languages are based on the lambda calculus, a core language involving only variables, constants, applications, and function abstractions. This similarity simplifies a lot of the translation process. Overall, the process maps Why3 constants to the target ITPs' constants, and preserves all other variables, application, and function structures. One exception unsupported by Isabelle is Why3's add-on feature, the as-binding used in pattern matching, which annotates a sub-pattern with a variable and binds the term captured by this sub- pattern the variable. We convert this into semantically equivalent let-bindings.
E.2 IMPLEMENTATION DETAILS
The implementation of the VC extraction and translation pipeline consists of six main components:
1. A Why3 patch to export Why3's internal Abstract Syntax Tree (AST) into an XMI. repre- sentation (in 200 lines of OCaml).
2. A Python parser to read the XML representation into an S-expression representation of an extended simply-typed lambda calculus (in 160 lines of Python).
3. Python library functions providing basic support for manipulating the lambda calculus, such as substitution, variable deconfliction, rewriting, and folding over atomic terms (in ~800 lines of Python).
4. A Python module for managing Why3 sessions, managing translation contexts (e.g., allo- cated constant/variable names in the context), and chaining all the components together to run them automatically (in 5500 lines of Python).
5. Translation rules, rewriting rules, ad-hoc term rewriting procedures, package management, and syntax check adapter, for each of the Isabelle, Lean, and Roeq (in 38000/7907700 lines of YAMI,, (9300/780997 lines of Python, for Isabelle, Lean, Roeq, respectively).
6. ITP libraries that map Why3 notions into the ITPs' native builtins (in ~50001100/000 lines of lsabelle/_ean/Rocq. respectively)
The subsection elaborates on some of the nontrivial components as follows.
The Why3 patch modified from Why3's existing Isabelle printer, which exports Why3 AST in XMI. format but with Isabelle-specific adaptations. We neutralize these adaptations to make output the raw Why3 internal AST. Specifically, we remove its mapping from Why3 terms to Isabelle terms; add Rocq and Lean keywords to the blacklist of variable names; fix its escaping of XML special characters; add support for the as as-binding syntax in pattern matching; add type annotations to definition exports.
The S-expression used in our internal process is a simply-typed (HOL style) lambda calculus ex- tended with native AST nodes for finite Cartesian products, pattern matching (the case statement), literal numbers and strings, and the as as-bindings (which bind the sub-term that matches a sub sub-pattern pattern
to variable, in a usual pattern matching). Bound variables represented in the same way as free
21

---

Published as a conference paper at ICLR 2026
variables; we do not De Bruijn indices, but instead maintain contextual variables and decon- flict names of bound variables explicitly (because it simplifies our parsing and printing work, while computational efficiency can be compromised in our context).
The substitution, variable deconfliction, and folding are all standard. We use Python's func- tional programming features to implement these operations. The rewriting system is simplified such that 1) all reducible expression (redex) patterns have the form (contant ary, ... argn) where all Isiy, are freee variables and the arity is schematic: to appear in the contractum, so the contracta can only be atoms or (nested) function applications. This simplification allows representing rewriting rule merely a tuple of the redex's constant name, the constant's 's arity, and list-represented S-expression for the contractum. We use YAML'S dictionary datatype to represent set of rewriting rules, e-g., (Why3 ennghh, 1, [Int. int, [Tsabell e length, aryol] ] rewrites (Why3.lenthe 1) into Int.int (Tsabelle.eenge f), for any 1. This greatly simplifies the writing of rewriting rules. For more complex rewritings that quire more complex redex patterns, we use hard-coded Python match-cas case to work over the S-expression directly.
lambda abstraction is allowed
PROMPTS
Our work employs two types of prompts: general prompts designed for broad-purpose LLMs and specialiZed prompts tailored for particular fine-tuned models.
The templates of the general prompts are shown as follows.
General Prompt for Isabelle
Given the following Isabelle theories as context, prove the Isabelle proposition given at the end.
File 'NTP4Verif.thy" (content of the theory file)
And many other libraries
File 'imp_Syee Saapp_SSSttttee.tuet thy"; (content of the theory file)
Given the context above, consider the proposition in the following Isabelle code: (the target proof goal together with its contextual theory)
Response the Isabelle proof only. Do not repeate any context nor the statement.
General Prompt for Lean
Given the following Lean 4 theories as context, prove the Lean 4 proposition given at the end.
File leass.lean':
(content of the theory file)
And many other libraries
File 'SymStateSet.lean' [content of the theory file)
Given the context above, consider the proposition in the following Lean code: [the target proof goal together with its contextual theory)
Response the Lean 4 proof only. Do not repeate any context nor the statement.
22

---

Published as a conference paper at ICLR 2026
General Prompt for Roeq
Given the following Roeq theories as context, prove the Rocq proposition given at the end.
File 'Basc.v:: (content of the theory file)
And many other libraries
File 'SymStateSet.v': [content of the theory file)
Given the context above, consider the proposition in the following Roeq code: [content]
Response the Rocq proof only. Do not repeate any context nor the statement.
The template specifically for Goedel-Prover and DeepSeek- Proverr is as follows.
Prompt for SpecialiZed Models
Complete the following Lean 4 code:
(the target proof goal together with its contextual theory)
Before producing the Lean 4 code to formally prove the given theorem, provide detailed proof plan outlining the main proof steps and strategies. The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.
G FAILURE CASES
To investigate the failure modes of NTP models on verification conditions, we analyzed the error logs and proof scripts from our evaluation. We highlight three dominant categories of errors: syn- tactic invalidity, semantic degeneration, and hallucination. It is important to note that the statistics presented below represent conservative lower bounds. For syntax and hallucination errors, proof assistants abort execution at the first error; thus, a single proof might contain multiple subsequent errors that remain uncounted. Similarly, our detection semantic degeneration relies on rigid reg- ular expressions for some common cases, likely missing more subtle forms of degeneration.
Generating syntactically well-formed terms remains a primary hurdle, particularly for complex nested expressions in VCs. In our analysis of Isabelle proof attempts, we found that at least 24% failed solely due to syntax errors. Listing shows the complete erroncous proof generated by DeepSeck-V3., for proving the correctness of the decompose Front_node node function trees. This function is responsible for decomposing the front node of an AVL tree, and its correctness specified by the corresponding VC. Specifically, the term seq (m1 1) represents the sequence of elements in the left subtree 1, d refers to the data element of the current node, and hgt (m1 first introduce the
AVL
r) denotes the height of the right subtree z. The generated proof attempts universally quantified variables d2 and res, followed by a case analysis on ol, which represents the structure of the AVL tree. However, the term cannot be parsed due to two subtle syntax errors: (1) a missing closing parenthesis in deeply nested arithmetic expression on line 16, and (2) two extraneous closing parentheses on lines 18 and 25, respectively. fact, if one only removes the last extraneous closing parenthesis, the term can be parsed. However, it will result in term in the form ".. A (0 < (1 + expr) - hgt (m1 resl) 1)1)))))))))) A ... which is syntactically valid but semantically incorrect (the height of I is being conjoined with another inequality). What one would expect is which requires removing the extraneous parenthesis line 16 and adding closing parenthesis after "resl". The lengthy logical formulas with deeply nested constructs is a common pattern in VCs, which poses significant challenges for NTP models to maintain long-range syntactic coherence.
instead -A (0 < (1 + expr) - hgt res1))
23

---

Published as a conference paper at ICLR 2026
lenna
Frent, Front_node
"fa
tixes 1: "'a t2"
fixees ol 1: v'a view*
fixee "ta t1
assunes racto: 1-int balancing E hgt
hgt 21*
assunes Factl:: "hgt iml 11 hgt (nl r) int belancing"
assunes fact2: "case ol of (MExpty ta vicx) # agt (ml 1) int) A....
shows
10
S hgt 1.11
11
and *Vid2 :: 'a til 1205 1: =2).
12
(case ol of IASmpty 11 view) = o2 d res -
13
ANode 11 d21 r2
(Rtres) +2). (node model lseg (m) 111) ...)i""
proof
15
16
fix d2 res
17
"case ol
18
reeg rest)t t0 S 11f hot imi 11) hot ima E2) ther het (m1 #2) clse hat (nl 111)) het ini rest)
r2 Bheest node (seg
leeg
19
20
(it hat (ll 111 hgt (nl #21 then hgt ml =2) eise agt iml 1131) hat (ml ceell $11 iml
21
node model (1 bot (ai sesll
st then hag (ml
hat z2s1)1)
cest
23
(it bgt (nl resl) bgt (ml F) ther. agt (ml r) cise agt iml resli>: bag inl reo) S 1) (-Int belancing hat (nl resl) het (al A hot (m2 resl) hot [nl Et g gint balancing - bot
24
25
(1f
205)
27
show "ooda_nodal (seg ini 13) tseg tnl 2)) Cors (seq Inc roal) A
28
(0 S (1 lir hot imi 11 hat tnl x) then Eat (nl x) clse bat (nl 1311 hat tml res) proof (cases
29
(it (nl
hat
31
case AEmpyy
32
with pre have de_d 122 dt and rea_dat: tres by simp_all
33
from fast [untoled AEmety] have "saq
and bet_l: (nn simp_all
35
show Itheais unfolding de_ dea_der
36
by isinp add: seq_1 rode_nedol_dat, auto simp: b facto factl)
37
next
case (ANode
39
with pro cbtain real where
40
decomp: "ncdc_nodel iseg ml 111) d21 reoq (n1 r2)1 Cons 02 (5eg (t1) posi)) and res_seq: by
nede_nodel (seq real)] (seq (nt
43
44
fron fast2 Juntlded MMode] have sec_l: 1) node_nodel by simp
45
(5oq (m1 12)1
47
48
show 2thesic
seq_l decoup zwa_sey nuske_odeel_ee. natia (mono_taga, lifting) fact2 case_prod_cavv)
51
ged
52
53
Listing 1:
The complete proof generated by DeepSeek-V3.1 for the correctness of the decompose front node function on AVL trees.
24

---

Published as a conference paper at ICLR 2026
lemna goall0 (z. Menory.aadr) [t_1 Memory.adds B) $t.4 Hemory.add: Senary,acdr) it
it Menory.addr -> 21 it_2 Menory-addr ->
lat 1_1 Wemory.
Kemory-ahi Ft. (1 207
Menory.addr Nenory.ehiftt
2)
let: x_1 2. 1__ a_2;
let
Menory.eddr Nemory-ehift
1et 8.4 Manery.addr Kenory.chift (3 B)r
10
let 8_5 Memory radde 1.4 9_
11
Nemory-
(Henory. hadrry.dddreeese. baster.bbeee... a) (0
-21147483688
(2147483647
Kemory rsanod esanny fxconstisi3:pp www.ttiispp..ild..... valid t.4 =.1 a senory.valid.. a.3 (1
Nenory,
Nenory, sesnst t_3 Cint.de_sinnie cint.is_
conory.valic.ue t a (1 Nenory. va id rd 1 ( XI -> Hemory. va i rd a.2 d. :. Axioont 2 valie enpty a.5 x
14
15
M momoet iKemory. empty IE_4
t_a (Cint.io_atne32 X_2)
16
18
intro 1 8 221 x 1 a.d a_5 Perriion toxe_lowe huxp_pperr hutraned E_L_idsed t_ sconnet huxcsinc16 h_valid rd h_valid_ro h_valid_rd_e pa.aaiddeee or_enpty__s
19
uintli
h_monset
have hLmain Axcomstici2. valss cnpoy t It_4 0_41 (ciat.to_uiatt)) X_2) by have h1 Anionatiol2-p p.p.. w.d........................ valid empty t (t.4 8.0 iCint to_ttttotttttt vint x.21 by franee"" stop hypothetioni and depends on
22
23
actimation 'iatinsttol2 wtt.alppppsliooo_oo_oooo oo_po_or
and now Interacts wich "enory, In practics, se might need noze specific information iemas to nake this stop rigerous. "tatreee"" oirectly implios conclusion.
26
27
have h2 :- h_framed
30
have h3 :- tinked
1" h_b_valid_memb
have 56 :- P_valia_rd__a]
34
have h7 1n F_valid_rd_a
35
h_valia_rissl
:- l_valid_rdda
have h10 :" "Lo_vval-1Lor_omtty..
38
have hil :- h_nonset
39
simp_all Axxionaci12.ppvvaaaa
Axiomatiel3, wtwp::iiiii......eaa.m nend, Manory. Craned,
Konory.linked, Moncey.
</> (tzy contradiction) <2>
42
43
Itzy
Itry assup!
<j>
46
(tzy
47
simp_all uiaats]
<i>
50
onaga
))
54
exact h1 hunnin
Listing 2: Example of semantic degeneration: Redundant variable renaming Lean proof.
25

---

Published as a conference paper at ICLR 2026
NTP models frequently lose track of the proof state, resulting in repetitive, meaningless steps. We detected this behavior by matching patterns continuous "renaming" (e.g., using have h1 h2 where both h1 and h2 simple identifiers) repeated at least three times. In Lean, more than 64% of proofs generated by Goedel-Provert Prover---ov22- V2-32B exhibited this specific degenera- tion pattern. Listing 2 exemplifies the generation of repetitive and meaningless tactic applications in Lean. The model
engages in a redundant "renaming ritual" (have h.2 h ameed, etc.), erroneously assuming that automated tactics like simp_a aa require local variable aliases to access the context. This behavior likely stems from domain shift, where the proof context more complex than the standard mathematical corpora used for training. Furthermore, the comments (e.g., "assume that h_ framed directly implies the conclusion") explicitly admit that the logical step hypothetical. This suggests inability to derive the necessary lemmas to complete the proof.
Models often invoke non-existent constants, lemmas, or tacties due hallucinations. For instance, GPT-o4-mini frequently attempts to solve Roeq VCs using why3 tactic, which does not exist in the language. In Isabelle, at least 9% of failures were triggered by references to undefined con- stants or lemmas that absent from the context. We identified these cases by explicitly matching keywords such as "Undefined fact" or "Undefined constant" in the error logs. Crucially, since the proof assistant terminates the checking process at the first encountered error, hallucinations present in the latter parts of proof scripts - especially those already halted by syntax errors or earlier tactic failures remain uncounted. Consequently, this 9% figure represents highly conservative lower bound.
H CLASSIFICATION & METRIC DETAILS OF TABLE 4
The operation classification is conducted on the Isabelle version of our benchmark. We developed Isabelle extensions analyze the expressions of the obtained proof goals. We elaborate the constitution of each category in Tab. 4 as follows.
Integer Arith consists addition, subtraction, multiplication, division, exponentiation, comparison, square root, and factorial operations whose operands are integers, natural num- bers, or bounded integers (machine integers); and also bit-width conversions and bitwise operations.
Non-linear Arith consists of multiplication, division, and exponentiation between constant expressions. following de Moura & Bjømnr (2008) and Z3 (2025). In Tab. 4, most cases contain distinet non-linear operator multiplication and sometimes contain additional operators like division and exponentiation.
Float Arith consists of arithmetics on floating-pon point numbers. All floating-poin numbers in our benchmark cases are modeled as real numbers, disregarding precision errors.
List, Sequence consists of operations involving the list type and Why3's sequence, a array31, array32 and array63.
Set, Map, Bag consists of operations whose types involve finite map, multiset, finite set, predicate-based set, and hash-table.
Tree, String, Matrix consists of operations whose types involve Why3's built-in binary tree, string, and matrix.
Memory consists of operations whose types involve Frama-C's memory encoding.
Custom Datatype consists of operations whose types involve any datatype not provided by the system library but defined by the verification projects.
The metric depth is the height of the abstract syntax tree of the VCs, in the standard X-calculus representation with all arguments every function application represented as siblings.
26

---

Published as a conference paper at ICLR 2026
I INTERSECTION ANALYSIS OF NTP AND HAMMER CAPABILITIES
To understand whether neural and symbolic ap- proaches overlap or diverge in their capabilities, we analyze the intersection between the union of all problems solved by NTP models and the union of all problems solved by hammers. Table presents the results. The results reveal com- plementarity: many verification conditions are solved exclusively by one method the other. This confirms that NTPs and hammers leverage distinct reasoning mechanisms and that neither approach is subset of the other, highlighting the potential for hybrid solutions.
Table 7: The number of problems solved by both hammers and NTP models, only by ham- mers, and only by NTP models.
Hammer
NTP
Category
Common
only
only
Algorithm
Data Structure Calculation
5
2
Engineering Competition
2
0
3
3
Function
Memory
17
Loop
16
0
J IDENTIFYING
Invalid Arg.
15
0
VCs IN COQSTOP AND FVEL
Total
27
87
7
In order to support the numbers given in Tab. 1, this section describes our approach to identifying VCs in the CoqStoq benchmark (Thompson et al., 2025) and FVEL (Lin et al., 2024). CoqStop's
test contains 10,396 theorems from 12 Roeq projects; FVEL's set contains 1967 cases.
CoqStop CoqStop's VCs are predominantly drawn from CompCert, which accounts for over 58% of the test set, while other verification-related projects constitute no more than 6%. There- fore, focus solely on CompCert. In CompCert, the tactics and other constructs that are rele- vant to program analysis and VC generation are TransfInst: UseTrans fer, monadInv, step simulation, exploit, and match states. Among the CompCert VCs in CogStop, only 1,325 cases involve these tactics, accounting for 12.7% the total test set. Including other projects that may involve VCs (at most 6%), the total proportion would not exceed 20%.
FVEL All of FVEL's test cases are extracted from seL4. seL4's VCs are generated using the tacties veg. wp. and wpsimp. Based on the test case list provided by FVEL, we analyzed cases whose proofs contain these tactics and found only 328. Therefore, the proportion of VCs in FVEI. does not exceed 328/1967 < 17%.
K THE USE OF LARGE LANGUAGE MODELS (LLMs)
We have used L.LM as a writing aid assist with fluency and grammatical checking.
27


Reviews:
[{"review_id": "lnjJO399WI", "reviewer": "Reviewer_eJD5", "summary": "This paper propose a challenging and real-world program verification benchmark, theorem proving for verification conditions (VCs). Different from most theorem proving benchmarks, VCs are the primary (and transient) intermediate representations of program verification in the real world. This work first collects VCs by instrumenting a popular program verifier, Why3, and then converting them into three popular interactive theorem provers (ITPs), i.e., Isabelle, Lean, and Rocq,  based on manually designed rules (around 800 for each ITP). The verification tasks span two categories: 1) small challenging puzzles that involve non-trivial data structures and algorithms, and 2) C programs from real-world projects. The experimental evaluations show that neural theorem provers (NTP) achieve less than 4% pass rate, which is consistently worse than classic ATPs like CoqHammer/Sledgehammer. The new benchmark remains challenging for both ITPs and ATPs, motivating technical innovations in both.", "questions": "How large are the translated theorems in ITPs? Is there always a single proof goal? Are they human readable?\n\nThe results presented in Table 5 are really interesting. Besides comparing the absolute number of solved theorems, are they complementary or roughly a subset of another?", "limitations": "", "rating": 8, "confidence": 5, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "- Constructing a real-world program verification benchmark using VCs is well-motivated and the paper is well-written. \n- The benchmark construction is based on high-quality expert-written rules, which is reliable and one-time effort. \n- The NTP4VC benchmark strikes a good balance of two categories of challenging program verifications, specifically, small programming puzzles and real-world projects. Furthermore, the transient nature of VCs make potential contamination less of a concern.\n- Experimental evaluations show the clear gap as well as promises of neural theorem provers, motivating future follow-up works.", "weaknesses": "- compared to programs and annotations at the source code level, VCs and relevant proofs are perhaps too low-level and less suitable for LLMs to generate proofs, since human experts rarely write proofs for VCs. Although NTP4VCs is an interesting and challenging benchmark, but may not be necessary to tackle directly by LLMs. The cost is also prohibitive, as indicated by the limited evaluation with GPT-o4-mini-high. \n- three themes of errors (presented in sec 5.2) are well expected; having a quantitative analysis will be more helpful.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "zvVA0JYuoe", "reviewer": "Reviewer_c1Bg", "summary": "The authors introduce NTP4VC, a novel benchmark targeting neural theorem proving (NTP) for program verification conditions (VCs). Unlike prior datasets focused on mathematical or auxiliary lemmas, NTP4VC consists of real-world VCs automatically extracted from industrial projects using mature verification pipelines. The benchmark covers multiple languages and a diverse range of verification scenarios, aiming to reflect practical challenges in automated program verification. Experimental results show that existing neural and automated provers perform poorly on NTP4VC.", "questions": "See Weaknesses", "limitations": "", "rating": 4, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "1. **Benchmark contribution:** \n\nThe authors introduce a new dataset specifically addressing VC proving, which is a practical bottleneck in automated program verification.\n\n2. **Industrial relevance:** \n\nVCs are extracted from real-world industrial projects using established verification pipelines (Why3, Frama-C), increasing practical relevance.\n\n3. **Multi-language and scenario coverage:** \n\nThe dataset spans multiple proof assistant languages and aims to cover a variety of verification scenarios.", "weaknesses": "1. **Limited dataset novelty:** \n\nAlthough the focus on VCs is clear, the novelty is moderate. Previous datasets (e.g., CoqStop, FVEL, CoqGym) have also included verification-related theorems, even if the VC proportion was lower. The paper should better highlight what fundamentally differentiates NTP4VC—beyond just the percentage of VCs.\n\n2. **Lack of technical contribution:** \n\nThe work mainly involves dataset construction and benchmarking; there is no new technical advance.\n\n3. **Provability not manually verified:** \n\nWhile VCs are generated using automated tools, there is no evidence of manual or sampled verification to guarantee their provability. This raises the risk that some VCs may be invalid or unprovable due to the toolchain.\n\n4. **No quantitative analysis of VC diversity:** \n\nThe paper focuses on diversity of program sources, but does not quantitatively analyze the types of generated VCs. It is unclear whether the dataset covers a broad range of VC properties or is dominated by a few repetitive types. A breakdown of VC categories/properties would strengthen the empirical evaluation.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "Pv1MIsDR2y", "reviewer": "Reviewer_B7qC", "summary": "The authors propose a benchmark for proving verification conditions. They extract these benchmarks from a combination of real world code, where the VCs are extracted using existing industrial tools, and are then simplified massively by removing hints like asserts and lemmas. The authors then evaluate existing LLMs, NTPs and Hammers.", "questions": "See weaknesses. Also:\n1. Have you thought about composing different VCs to try and create even more complex benchmarks?\n2. How easy is it to add more projects to the set of real-world verified programs?\n3. Can you elaborate on your statement in lines 403 -- 408? I am not sure I really understand why one category performs better than the other.", "limitations": "", "rating": 4, "confidence": 4, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "1. The work is novel to the best of my knowledge, and addresses a fundamental gap: automating program verification for real-world complex programs.\n2. Thorough evaluation of models and NTPs on the generated datasets. I also appreciate the datasets being created for different languages.", "weaknesses": "1. Lack of details on how the 5.3K VCs get filtered down to 627: I'm not sure why this was done, or what were the criteria for eliminating majority of the VCs. Were they too similar to each other, making them redundant? Or was it some deeper issue? Regardless, the elimination process was not described in the paper. Furthermore, out of the 5.3K, how many were extracted from the real-world programs and how many were extracted from the pearls of programs?\n2. The pearls of programs: Does the inclusion of these pearls of programs not contradict the real-world claim of the title of the paper? I understand the need for diverse VCs, but the pearls seem more as an exercise in niche settings rather than VCs that occur frequently in realistic programs.\n3. Discussion centered around improving NTPs: I would like a discussion that focuses on how NTPs could improve on such VCs. I assume that these VCs would be difficult to prove even for humans. Even if one would try to perform RL, the initial accuracies of NTPs are not enough to provide straightforward gains. How could one try to improve NTPs on such complex benchmarks?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "glRB14lnhp", "reviewer": "Reviewer_MX3g", "summary": "The paper introduces NTP4VC, a new task and benchmark that targets neural theorem proving of verification conditions (VCs)—arguably a core bottleneck in automated program verification. The authors (i) extract VCs from real-world projects via industrial pipelines (Why3/Frama-C), (ii) translate them with ~2.4K expert-written mapping/rewriting rules into three ITPs (Lean, Isabelle, Rocq), (iii) complicate the VCs by erasing helper annotations to make proofs harder while remaining provable, and (iv) evaluate LLM provers and hammer baselines. The released benchmark contains 672 VCs spanning pearls (algorithms/data structures) and real C verification (Contiki OS, Linux scheduler, etc.), with difficulty balanced so Why3’s strongest ATP tactic hovers around ~20% success. Across languages, modern LLM provers achieve <4% pass@8 while Isabelle/Coq hammers perform better but still modestly (up to ~15% pass@1).", "questions": "1. From >5.3k extracted VCs, 672 are “carefully selected,” but criteria are only qualitatively described. Can you please release the full pool with metadata (size, quantifier alternation, AST depth, symbol counts, dependency graph) and the sampling procedure?\n\n2. For a representative subset, can you show end-to-end proofs exist in at least one target ITP (perhaps with generous hammer help), confirming that difficulty stems from complexity rather than unprovability introduced by erasing?", "limitations": "", "rating": 6, "confidence": 2, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "1. Problem focus is well-motivated. VC theorem proving sits at the heart of verification workflows and is less explored by NTP than math benchmarks. By targeting VCs directly (rather than only annotation synthesis), the paper addresses a real bottleneck and usefully complements recent annotation-centric efforts such as Laurel and DafnyBench. \n\n2. Extracting from Why3/Frama-C, translating to Isabelle/Lean/Rocq, and sourcing from Contiki/Linux bring the setting closer to practice than e.g., purely math (miniF2F/PutnamBench) or toy code-property suites.  The two halves (pearls vs. real C) and per-category balancing around a target ATP pass rate are thoughtfully constructed; the complication step measurably increases hardness. \n\n3. Results convincingly show VCs are qualitatively harder for current NTP models than math/formal benchmarks.", "weaknesses": "1. Concerns regarding translation correctness: The benchmark depends on ~2.4K hand-written translation/rewriting rules and occasionally axiomatizes termination when Isabelle/Rocq can’t discharge it. There is no formal correctness proof of the translation or quantitative post-hoc validation beyond syntax checks/cross-review, leaving risk of subtle semantic drift or unsoundness through added axioms. A minimal mechanized proof of semantics-preservation for a core calculus would be beneficial.\n\n2. Contamination analysis is qualitative. Given that “engineering” cases show unusually high NTP success relative to others, please run decontamination (code/proof snippet search against common training corpora) to support the low-contamination claim.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)