Organizations: State Key Laboratory of Novel Software Technology, Nanjing University, China · School of Computer Science, Nanjing University, China · Department of Computer Science, ETH Zurich, Switzerland · School of Computing and Mathematical Sciences, Birkbeck, University of London, UK
Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual and limits scalability. Advances in large language models (LLMs), especially in mathematical reasoning, make their integration into software verification increasingly promising. This paper introduces a neuro-symbolic proof generation framework designed to automate proof search for system-level verification projects. The framework performs a best-first tree search over proof states, repeatedly querying an LLM for the next candidate proof step. On the neural side, we fine-tune LLMs using datasets of proof state-step pairs; on the symbolic side, we incorporate a range of ITP tools to repair rejected steps, filter and rank proof states, and automatically discharge subgoals when search progress stalls. This synergy enables data-efficient LLM adaptation and semantics-informed pruning of the search space. We implement the framework on a new Isabelle REPL that exposes fine-grained proof states and automation tools, and evaluate it on the FVEL seL4 benchmark and additional Isabelle developments. On seL4, the system proves up to 77.6% of the theorems, substantially surpassing previous LLM-based approaches and standalone Sledgehammer, while solving significantly more multi-step proofs. Results across further Isabelle benchmarks demonstrate strong generalization, indicating a viable path toward scalable automated software verification.
Figures & tables
Figure 1: An example theorem and its human-written proof from the seL4 project, shown alongside LLM-generated attempts. The human-written Isabelle proof illustrates the procedural, tactic-driven reasoning style that is common in software verification. We prompted two state-of-the-art LLMs, Gemini 3 Pro and GPT-5.1, to synthesize the same proof under controlled conditions, with web search disabled to avoid any leakage of the original script. Although both models correctly recognized the proof context and invoked some relevant tactics, neither succeeded in producing a valid proof even after roughly one minute of internal reasoning. Their attempts frequently misuse the domain-specific wp tactic, or hallucinate nonexistent lemmas.
Figure 2: Overview of our neuro-symbolic proof-search framework. Starting from the initial proof state, the system repeatedly generates candidate proof steps using a fine-tuned LLM, followed by rule-based symbolic revision to repair syntactic or semantic issues in the proposed steps. Each accepted step is executed by Isabelle/HOL to derive new proof states, which are then filtered by symbolic tools to prune states containing counterexamples or duplicates. The remaining states are ranked using cumulative LLM log-probabilities, and the highest-scoring ones are selected for further expansion in a best-first search. If the search cannot complete the proof, the framework finally invokes Sledgehammer to attempt to resolve the remaining goals.
Method
Val
Test
TsHd
Total
Neural
Selene
6.1
7.0
3.3
5.6
FVEL
8.9
9.5
4.5
7.8
Symbolic
Auto
4.9
6.7
6.1
5.9
Hammer
40.5
39.5
40.9
40.3
Ours
Qwen3
73.6
74.9
61.1
70.4
Δ
↑ 33.1
↑ 35.4
↑ 20.2
↑ 30.0
Table 1: Proof success rates (%) across validation (Val), test (Test), and test-hard (TsHd) splits. Compared to existing neural and symbolic provers, our framework delivers substantial improvements: Qwen3-1.7B achieves 70.4% overall success, and Mistral-7B reaches 77.6%, exceeding the strongest baseline by 30.0 and 37.3 percentage points, respectively.
Figure 3: Proof success rate across ground-truth proof lengths. Our approach consistently outperforms existing methods. In particular, the success rate decreases as proofs grow longer, but our approach still maintains non-negligible performance even on proofs exceeding 10 lines.
Figure 4: Proof success rates across the six seL4 session categories. Our approach yields stronger performance than all baselines in all sessions. Notably, it achieves high accuracy even on the challenging SysInitGroup category, which is entirely unseen during training.
Method
# of proof lines
% of coverage
Selene
197
1.1
FVEL
271
1.6
Auto
204
1.2
Hammer
2,581
15.0
Ours
6,235
36.2
Table 2: Coverage results of automatically generated proof lines. Our method attains the highest coverage, proving theorems whose existing proofs amount to over one-third of all proof lines and substantially outperforming existing baselines in reducing manual proof-script development effort.
Figure 5: Proof completion rate under varying proportions of expert-provided proof lines. Our method is increasingly effective as more human-written lines are supplied. Overall, the method reduces human effort by 71.1% on average.
Figure 6: Sequence and Jaccard similarity between generated and ground-truth proofs across proof lengths. Both metrics remain low and decrease as proofs grow longer, suggesting the model synthesizes novel strategies rather than recalling memorized proofs.
Figure 7: Performance of our proof search framework on additional benchmarks. The x -axis lists the benchmarks, where entries in brackets denote the number of theorems included in each benchmark. Our approach consistently achieves higher proof success rates across all benchmarks, demonstrating strong generalizability and robustness.
Method Variation
Rate
DeepSeek (DpSk) v3.2
5.5
DpSk + Tree Search
12.5
DpSk + RAG + Tree Search
33.0
DpSk + RAG + Tree Search + Hammer
52.0
Ours (Trained LLM + Tree Search + Hammer)
70.0
Table 3: Proof success rate (%) on several variants of our framework. The proof success rate increases progressively as tree search, retrieval augmentation, and hammer are incorporated, indicating the necessity of each component. The comparison highlights that our full approach, which replaces the off-the-shelf model with a fine-tuned LLM, achieves substantially stronger performance.
Method Variation
Rate
Mistral-7B + Tree Search
0.0
Qwen3-1.7B + Tree Search
0.1
Mistral-7B SFT + Tree Search
59.8
Qwen3-1.7B SFT + Tree Search
57.1
Table 4: Effect of supervised fine-tuning under the same tree-search configuration. Without fine-tuning, the base models solve almost no theorems; in contrast, after supervised fine-tuning, both models reach around 60% proof success.
Error category
Count
%
Error category
Count
%
Undefined fact
3,263,494
60.1
Bad method args.
65,430
1.2
Tactic inapplicable
976,398
17.9
Inner syntax error
50,033
0.9
Multi-line / other
423,982
7.8
Undefined method
47,163
0.8
Unknown variable
161,842
2.9
Proof unfinished
37,100
0.6
Outer syntax error
153,037
2.8
THM exc.
26,750
0.4
Type unification
110,717
2.0
Undefined constant
8,852
0.1
Table 5: Step-level error breakdown over all tactic attempts on the validation failures (241 theorems, 7.77M attempts). Undefined-fact alone accounts for nearly two-thirds of all errors: the LLM repeatedly cites premises that do not exist in the active context.
Max search depth reached
Theorems
%
0 (no progress past initial state)
11
2.4
1 – 10 (early stall)
6
1.3
11 – 30 (medium-depth stall)
109
24.2
31 – 60 (deep stall)
181
40.1
>60 (very deep)
145
32.0
Total
451
100
Table 6: Search-depth distribution for failures on the test and test-hard splits (the validation log format does not record depth markers). Only 3.7% of failures stall before depth 10; most failures make substantial multi-step progress and run out of budget later in the search.