Paper deep dive
Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification
Baoding He, Zenan Li, Wei Sun, Yuan Yao, Taolue Chen, Xiaoxing Ma, Zhendong Su
Intelligence
Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 97%
Last extracted: 3/23/2026, 12:08:31 PM
Summary
Stepwise is a neuro-symbolic framework for automated systems-level software verification that integrates Large Language Models (LLMs) with Interactive Theorem Provers (ITP). It utilizes a best-first tree search over proof states, where an LLM predicts the next proof step, and symbolic tools (Isabelle/HOL, Nitpick, QuickCheck, Sledgehammer) handle step revision, state filtering, and goal discharge. The framework achieves a 77.6% success rate on the seL4 benchmark, outperforming previous LLM-based approaches.
Entities (6)
Relation Signals (4)
Stepwise ā evaluatedon ā seL4
confidence 100% Ā· evaluate it on the FVEL seL4 benchmark
Stepwise ā uses ā Isabelle/HOL
confidence 100% Ā· We implement the framework on a new Isabelle REPL
Stepwise ā integrates ā LLM
confidence 95% Ā· This paper introduces a neuro-symbolic proof generation framework designed to automate proof search
Sledgehammer ā partof ā Stepwise
confidence 90% Ā· if the tree search still fails to resolve the goal, Sledgehammer acts as a backstop
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract: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 systems-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 benchmarks demonstrate strong generalization, indicating a viable path toward scalable automated software verification.
Tags
Links
- Source: https://arxiv.org/abs/2603.19715v1
- Canonical: https://arxiv.org/abs/2603.19715v1
Trouble viewing inline? Open PDF directly ā
Full Text
76,165 characters extracted from source content.
Expand or collapse full text
Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification Baoding He 1,2,ā Zenan Li 3,ā Wei Sun 1,2 Yuan Yao 1,2,ā Taolue Chen 4 Xiaoxing Ma 1,2,ā Zhendong Su 3 1 State Key Laboratory of Novel Software Technology, Nanjing University, China 2 School of Computer Science, Nanjing University, China 3 Department of Computer Science, ETH Zurich, Switzerland 4 Department of Computer Science, Birkbeck, University of London, UK Abstract Formal verification via interactive theorem proving is increas- ingly 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 pa- per introduces a neuro-symbolic proof generation framework designed to automate proof search for systems-level verifi- cation 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 syn- ergy 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, sub- stantially surpassing previous LLM-based approaches and standalone Sledgehammer, while solving significantly more multi-step proofs. Results across further benchmarks demon- strate strong generalization, indicating a viable path toward scalable automated software verification. 1 Introduction Formal verification plays a vital role in ensuring the correct- ness and reliability of software systems, especially in safety- and security-critical domains where failures can be catas- trophic [1,2,3]. Interactive theorem proving (ITP) stands out for its expressiveness and ability to provide the strongest assurance. With ITPs, landmark projects such as CompCert (a 1 These authors contributed equally to this work. 2 Corresponding authors. formally verified optimizing C compiler whose correctness is mechanically proven in Rocq [4]) and seL4 (formally verified OS microkernel whose functional correctness, security proper- ties and reliability guarantees are proven in Isabelle/HOL [5]) have been successfully delivered, which demonstrate that for- mally verified systems can achieve both practical usability and rigorous correctness. While ITP offers unparalleled assurance, it also incurs substantial costs, preventing its wide adoption, especially in large-scale, systems-level software [6]. Specifically, a typical software verification workflow involves 1) writing precise formal specifications to be proved and 2) constructing rig- orous proofs for these specifications, both of which demand immense human effort. For example, the seL4 verification project required approximately 20 person-years of work, and produced over 100K lines of proof scripts, compared to only about 10K lines of C implementation and merely 3K lines in its simplest abstract specification in Isabelle [5]. More- over, developing such specifications and proofs necessitates specialized expertise in both theorem proving and the target domain, a combination that is challenging to acquire. In this work, we focus on the proof generation step in systems-level software verification projects. Recently, large language models (LLMs) have demonstrated encouraging mathematical reasoning capabilities, which inspire research into their application for software verification, particularly for proof generation [7,8,9,10]. Unfortunately, both prior studies and our initial experiments show that, even when theorem statements are well formalized and relevant libraries are fully provided in advance, current LLMs still struggle to generate complete, correct proofs. We summarize two challenges as follows. ā¶Lack of specialized expertise. The first challenge lies in that software verification often relies on numerous domain- specific lemmas and specialized proof tactics. Although mod- ern LLMs perform well in general reasoning tasks, they are not well-versed in these specialized domains, leading to lim- ited effectiveness when applied to proving corresponding the- orems. For example, LLM4FSCQ [7] evaluated models such 1 arXiv:2603.19715v1 [cs.AI] 20 Mar 2026 as GPT-4o and Gemini 1.5 Flash on FSCQ (a Rocq-based file system verification project [11]) and achieved only 38% proof coverage. Moreover, in the larger seL4 project, which involves extensive lemma libraries and customized tactics, Selene [9] found that GPT-4 succeeded on only 20% of a benchmark theorem set, despite the fact that nearly 40% of them require one-line proofs. ā·Pausity of usable data. The second challenge, which is closely related to the first, is the shortage of high-quality (training) data for software verification. For instance, the seL4 project contains only around 20K theorems and lemmas, and most proofs are written in a procedural style, where much of the reasoning is implicit and encoded in the interaction with the theorem prover. This substantially limits their usefulness in effective LLM training/fine-tuning. Indeed, FVEL [10], which systematically extracted theorems from seL4 to fine- tune Mistral-7B-Instruct [12] and Llama-3-8B-Instruct [13] models, reported a success rate below 10% (88 out of 1,077 theorems in the test set). 1 Approach. In this paper, we propose a proof generation frame- work that synergistically combines LLMs and ITPs, aiming for automated systems-level software verification. Our ap- proach adopts a proof step-based tree-search pipeline that iteratively queries a fine-tuned LLM to predict the next proof step until the target theorem is successfully proved. To address the first challenge, our framework adopts a neuro-symbolic approach tailored to the nature of software verification. First, to address challenges posed by domain- specific lemmas and tactics, we incorporate a proof-step re- vision module that repairs or refines LLM-generated steps whenever they fail to compile or make no progress. Sec- ond, to efficiently prune unpromising branches, we utilize Nitpick [14] and QuickCheck [15] to ātestā each candidate proof state and discard those that admit counterexamples; the remaining candidates are then ranked by the LLM according to their plausibility. Finally, if the tree search still fails to resolve the goal, Sledgehammer [16] acts as a backstop that scans the local library for potentially relevant lemmas and attempts to complete the current proof. To address the second challenge, our tree-search pipeline facilitates direct interaction between the LLM and the theo- rem prover, by extracting the proverās internal proof state to LLM, which can inform and guide subsequent step predic- tions. This pipeline also enables ābootstrappingā training data generation. Namely, during the tree-search process, training data for proof-step prediction can be extracted on-the-fly. For example, if a theoremās proof consists of five steps, a success- ful tree search could yield five training instances, which can later be used for, e.g., fine-tuning [17, 18]. Experiments. We evaluate our framework on seL4 [5] proof 1 Selene only extracts a small subset of the seL4 project, and its collected theorems are relatively easy, with proof lengths ranging from one to five. In contrast, the FVEL benchmark is more comprehensive and challenging, as it extracts all the theorems to be proved from seL4. construction. The results show that, with a fine-tuned lan- guage model, our approach achieves a total proof success rate of up to 77.6%, significantly surpassing prior automated proof-generation approaches for seL4. Noteably, it excels, compared to the two preceding systems, at successfully han- dling a larger number of multi-step proofs, a challenge that has not been addressed by prior work. Moreover, our framework substantially alleviates manual proof-engineering effort, re- ducing expert proof-writing effort by 71.1% on average in an AIāhuman collaboration setting. Finally, experimental results on benchmarks from Archive of Formal Proofs projects (e.g., X86 Semantics , IEEE Floating Point, and SATSolverVerifi- cation), as well as the code verification benchmark Code2Inv (by translating its loop invariants into Isabelle theorems) con- firm the strong generalizability of our approach. Summary of main contributions. (1) We provide a neuro- symbolic framework based on LLM-enabled tree search, tailored for real-world, systems-level software verification projects. (2) We implement concrete integration of LLMs and a broad range of symbolic, logic-based tools, substantially enhancing the efficacy of proof-tree search; (3) We curate training datasets and benchmarks, and carry out thorough empirical evaluations. Our work advances a new frontier of AI4Verification, an emerging area focused on applying cutting-edge AI techniques to hardware/software verification, especially to support large-scale proof engineering for safety- critical systems and architectures. Structure. Section 2 illustrates the challenges of the problem. Section 3 presents our neuro-symbolic approach. Section 4 reports the evaluation of our approach on seL4 and four ad- ditional repository-level benchmarks. Section 5 reviews the related work. Section 6 discusses the limitations of the current work and outlines directions for future research. Section 7 concludes the paper. 2 Problem To show why existing LLMs struggle to synthesize proofs in real-world software verification tasks, we present a repre- sentative theorem from seL4. We choose seL4 as it remains the most comprehensive and influential milestone for sys- tem software verification. Its entire C implementation is proven functionally correct against a formal specification in Isabelle/HOL, ensuring the absence of crashes and undefined behavior. Building on this foundation, seL4ās verification was extended to enforce noninterference of information flows and access control, establishing formal guarantees of confidential- ity and integrity. To date, seL4 remains one of the safest OS kernels with machine-checked proofs of both implementation- level correctness and security properties, setting the bench- mark for formal system verification. An example from seL4ās verification is demonstrated in Figure 1, where the theoremcap_swap_valid_objsis drawn 2 theoremcap_swap_valid_objs[wp]: āā¦valid_objs and valid_capc and valid_capcā and tcb_cap_validc b and tcb_cap_validcāaā¦ cap_swapc a cā b ā¦Ī»rv.valid_objsā¦ā (* When there are no dangling pointers in the address space of the seL4 microkernel, for two valid capability slotsbelonging to two thread control blocks, swapping the contents of two capability slots preserves the absence of dangling pointers.*) apply (simp add: cap_swap_def) apply (wpset_cap_valid_objs | simp split del: if_split)+ done Humanexperts: write out the proof steps: tactics (e.g., wp) and lemmas (cap_swap_def) proof (prove) goal (1 subgoal): 1. ā¦valid_objs and valid_capc and valid_capcā and tcb_cap_validc b and tcb_cap_validc' aā¦ cap_swapc a c' b ā¦Ī»rv.valid_objsā¦ proof (prove) goal (1 subgoal): 1. ā¦valid_objs and valid_capc and valid_capcā and tcb_cap_validc b and tcb_cap_validc' aā¦ do y <-set_capc' a; y <-set_capc b; ... ... ā¦Ī»rv.valid_objsā¦ proof (prove) goal: No subgoals! Theorem prover: verify each proof step and propagate (forward) the proof state. Large language model: substitute human experts to automatically generate proofs Failed to finish proof: goal (7 subgoals): 1. āy yaslot1_p ... ... ā GPT ### Prove the following Isabelle statement. ### Input: lemma cap_swap_valid_objs[wp]: ... ... ### Response: This lemma comes from the seL4 kernel verification context ... ... apply (simp add: cap_swap_def) apply wp apply clarsimp done The user wants a proof of the lemma, likely in the seL4 Isabelle/HOL... apply (rule hoare_seq_ext) apply (wp set_cap_valid_objs set_cdt_wpdo_extended_op_wp set_original_wpgets_wp | simp add: bind_assoc)+ apply (wp | wpc| simp add: bind_assoc)+ Undefined fact: "hoare_seq_ext" ā 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 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. from the invariant proofs of the abstract specification of the seL4 microkernel, and similar proof patterns recur throughout the project. To prove this theorem, human experts write down (in Isabelle) three proof steps, each comprising one tactic (e.g., simpandwp) and some used lemmas (e.g.,cap_swap_defand set_cap_valid_objs; cf. the left panel in Figure 1). Unlike formal mathematics, theorems in software verifica- tion are often formulated as Hoare triplesP C Q, where PandQare the pre- and post-conditions, andCdenotes the program being executed. In seL4, the abstract behavior of kernel operations is modeled in a monadic style that yields imperative-like programs; the corresponding Hoare rules cap- ture the semantics of these monadic computations. Intuitively, the targeted theorem states that if the address space of the seL4 microkernel contains no dangling point- ers (valid_objs), then swapping the contents of two valid capability slotscandcā, which belong to two thread con- trol blocks (tcb_cap_valid c bandtcb_cap_valid cā a), remains dangling pointers free. Namely, after the opera- tioncap_swap c a cā bwhich exchanges the capabilities stored in these two slots, the resulting program state still satisfiesvalid_objsexpressed by the postconditionĪ»rv. valid_objs where rv denotes the return value of cap_swap. To reduce the burden of manually constructing proofs, de- velopers typically prepare a collection of broadly applica- ble tactics and lemmas, dedicated to software verification. For example, thewptactic, short for weakest precondition, generates the verification conditions associated with a given Hoare triple. During this process,wpsystematically ap- plies a suite of previously proved lemmas, each of which encodes a weakest-precondition characterization for a spe- cific construct or monadic computation. After a routine use ofsimpto unfoldcap_swap, human experts can then eas- ily invoke the pre-defined tacticwptogether with the lemma set_cap_valid_objs. In this example, the target theorem is discharged by combin- ing the tacticswpandsimp. The simplification step performs splitting, but the usual splitting rule forifis disabled to avoid unnecessary case distinction. In the proof script, the symbol |indicates that the tactic may apply either branch (or both), while the trailing+instructs it to repeat this process until no further progress is possible. This interleaving enableswp to generate obligations thatsimpcan reduce, whilesimpre- shapes the goals to facilitate subsequentwpreasoning. In this case, the combined step eliminates the goal entirely, and the proof concludes with done. To assess LLMs in generating this proof automatically, we experiment with two state-of-the-art proprietary models, i.e., Gemini 3 Pro [19] and GPT-5.1 [20]; their results are shown on the right panel of the figure. While both deep- thinking models successfully recognize the seL4 proof con- text, they are unable to apply the domain-specific tacticwp correctly. They also hallucinate lemmas that do not exist in the library (e.g.,hoare_seq_ext). We further attempted sev- eral rounds of iterative repair by feeding back the ITPās error messages, but the regenerated proofs continued to fail veri- fication. An analysis of the modelsā reasoning traces shows that they frequently misinterpret the functionality and per- formance characteristics of thewptactic and related lemmas (such as set_cap_valid_objs). 3 Initial State 0 Step 0 Step 2 Step 3 State 1 score: 0.7 Step 4 State 2 Score: 0.2 Step 6 Step 5 State 3 Score: 0.5 Proof state Ranking + Filtering Counterexample exists ... ... ... ... Final State Done or proved by Sledgehammer Proof step Generation + Revision Step 1 Error in execution file:///Users/zenan/Downloads/Untitled.html1/1 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. There are two potential approaches to addressing this is- sue. The first is to use retrieval-augmented generation [8,21]. In this paradigm, given a target theorem, a retrieval mod- ule searches for relevant or structurally similar theorems and proofs, which are then supplied to the LLM as contextual guidance. However, this strategy depends on both a high- quality proof corpus and an effective retrieval model: require- ments that are difficult to satisfy in our setting. For example, in seL4, when developers introduce a new module (such as SysInit, as shown in our evaluation) together with its accom- panying proofs, comparable proofs are often absent from ex- isting libraries. Moreover, even when analogous theorems do exist, neither model-agnostic nor model-dependent retrieval techniques reliably identify them within a large verification codebase [22,23]. In such cases, weak retrieval can degrade, rather than improve, the quality of generated proofs. Another approach is to fine-tune LLMs on collected proof data. This method is considerably easier to implement and has already demonstrated promising results in formal math- ematical proving. However, fine-tuning a model to directly generate complete proofs for software verification remains highly challenging. First, even in seL4, the available corpus consists of only about 20K theorems, which severely limits the effectiveness of fine-tuning. Second, unlike formal mathematics, most proofs in systems like seL4 are procedural: as our example illustrates, their true semantics reside implicitly in the the- orem proverās internal proof states rather than in the proof scripts themselves. As a result, LLMs struggle to acquire the necessary reasoning signal from surface-level proof text alone, making this approach impractical for now. 3 Methodology We propose a neuro-symbolic approach for proof step search on systems-level theorems. The overall procedure is illus- trated in Figure 2. Starting from the root node, which rep- resents the initial proof state, the search alternates between proposing new steps and deriving new proof states by execut- ing those steps within the ITP. To construct the next set of candidate proof steps for the cur- rent proof state, we first prompt a fine-tuned LLM to generate potential steps, and then apply a rule-based revision to refine or fix any imprecise suggestions. After executing these steps and obtaining a collection of new proof states, we introduce a hybrid mechanism to identify the most promising ones for further exploration. Specifically, we apply QuickCheck [15] and Nitpick [14], which serve as counterexample generators that help detect false conjectures or invalid intermediate proof states in Isabelle/HOL, to discard any proof state that contains a counterexample. We then use the LLMās prediction score (cumulative perplexity) to rank the remaining states and select the most promising one. Finally, if the search for the proof fails, we invoke an automated tool, i.e., Sledgehammer, to attempt to complete the proof. Putting all the above together, we establish the framework in Algorithm 1. 4 Algorithm 1 Proof Search Framework Require:initial states 0 , neural generatorG, symbolic checkerC , max iterations I max 1: initialize tree T with root containing s 0 2: for each iteration iā [1, I max ] do 3:nā highest_score_unexplored(T ) 4:succStatesā []; failStatesā [] 5:candidatesāG(n.state)ā· step generation 6:for each step Ī“ā candidates do 7:sā apply(Ī“, n.state)ā· ITP execute 8:if s is error state then 9:failStates.add((s, Ī“, log p Ī“ )) 10:else 11:succStates.add((s, Ī“, log p Ī“ )) 12:for each (s, Ī“, log p Ī“ ) in REVISE(failStates) do 13:sā apply(Ī“, n.state) 14:succStates.add((s, Ī“, log p Ī“ )) 15:for each (s, Ī“, log p Ī“ ) in succStates do 16:if s has no subgoals then 17:return proof scriptā· proof completed 18: ifC(s)detects duplicate or counterexample then 19:continueā· state filtering 20:scoreā combine(n.score, log p Ī“ )ā· scoring 21:insert_node(T , (s, score)) 22: return FAIL 3.1 Proof Step Generation & Revision 3.1.1 Proof Step Generation Our approach begins by generating candidate proof steps through prompting a fine-tuned LLM. Given the current proof state, which encapsulates the available hypotheses and the target goal, we query the model to propose the next proof step using a simple instruction template: ### Given the following Isabelle proof state, suggest the next proof step. ### Input: <current_proof_state> ### Response: <next_proof_step> The rationale for focusing on the current proof state is twofold. First, automated theorem proving can be cast as a sequential decision-making problem, and thus can be mod- eled as a Markov decision process, in which a standard result stipulates that pure, history-independent polices (i.e., the next step depends solely on the present state) suffice for the reach- ability objective, i.e., to reach the āproof doneā state. This is also a common practice in the literature of proof search, which turns out to be critical for efficiency [24,25,26]. Sec- ond, the structure and vocabulary of the proof state provide strong cues regarding which tactics are applicable and which premises are likely to be relevant [27,28]. Additionally, we focus on predicting a single step at a time. This is because, although multi-step prediction is possible in principle, the complexity of real proofs and the limited amount of available data make such predictions considerably more challenging; empirically, one-step prediction yields more reliable results. To fine-tune the model to predict such next steps, we con- struct a dataset of stateāstep pairs extracted from existing theorems and their complete proofs. Each proof is decom- posed into individual proof steps and replayed in the ITP, allowing us to record the intermediate proof state preceding every step. Using these aligned pairs, we fine-tune the LLM to generate outputs that are not only syntactically correct but also semantically sensible. Finally, since proof search de- mands efficient generation, we employ relatively small LLMs (e.g., 1.7B or 7B size), which are nevertheless sufficient for our specific tasks. 3.1.2 Proof Step Revision Writing syntactically and semantically valid proof steps in an ITP (such as Isabelle) is challenging, particularly in system verification tasks that depend on numerous domain-specific lemmas and tactics. Consequently, even a well-trained LLM may generate steps that either refer to premises or tactics ab- sent from the current proof context, or cannot be applied to the current goals due to syntactic errors or lack of progress. Such failures substantially degrade the effectiveness and efficiency of the proof search. Despite their incorrectness, these failed attempts often con- tain useful information. Continuing our running example, an LLM might identify relevant premisescap_swap_defbut pair them with an inapplicable tacticby; or it may propose a promising tacticwpwhile selecting premiseshoare_seq_ext that do not precisely fit the context. To fully exploit these incorrect but reasonable responses from LLMs, we employ a best-effort repair procedure. When- ever the ITP rejects an LLM-generated step, we record it for post-processing and re-evaluate the revised version. After examining all proposed steps for a given proof state, we sys- tematically transform the failed ones in two ways: (1) tactic repair: we extract the premises referenced by misused tactics and recombine them with a curated set of frequently used tac- tics; and (2) premise repair: we search the proof context for similar premises and substitute them where appropriate. By synthesizing additional candidate steps, these symbolic revi- sions help reveal prover-accepted steps, thereby strengthening the overall proof search. For the tactic repair, we first extract all tactics from the training corpus. Given a proof step rejected by the ITP, we attempt to rewrite it by identifying the premises referenced in the failed step and recombining them with the pre-built tactic set. As to the premise repair, which explicitly targets proof steps that fail with an āundefined factā error, we attempt 5 Algorithm 2 Proof-step revision and execution Require: Failed proof state set failStates 1: revisedStepsā [] 2: premiseSetā established from trainingCorpora 3: tacticSetā established from trainingCorpora 4: for each (s, Ī“, log p Ī“ )ā failStats do 5:if s.error is w.r.t. tactic thenā· tactic repair 6:pā extract referred premises in Ī“ 7:revisedSteps.add(combine(tacticSet, p)) 8:if s.error is w.r.t. premise thenā· premise repair 9:t/ pā extract referred tactic/premises in Ī“ 10:p ā² ā retrieve similar premises from premiseSet 11:revisedSteps.add(combine(t, p ā² )) 12: return revisedSteps to correct every LLM-generated undefined premise using an available version from the proof context. Concretely, we compare the undefined fact with all candidate premises using edit distance and select the closest matches (e.g., the top three). The failed step is then revised by substituting the matched premises for the undefined ones. The procedure of proof-step revision is summarized in Al- gorithm 2. However, the revision can produce a large number of candidate steps. To alleviate this, we impose constraints to keep the search space manageable. For tactic repair, we limit the tactic set (e.g., to the 12 most frequently used tac- tics). For premise repair, we pre-select a compact subset of premises from the library. In particular, we use MePo (a heuristic module in Isabelleās Sledgehammer that ranks and selects premises relevant to a given goal) as a lightweight relevance filter to retrieve the 128 facts most related to the current subgoal. 3.2 Proof State Filtering & Ranking 3.2.1 Proof State Filtering To alleviate state explosion in tree-search approaches, we reorganize the accumulated proof states before further ex- ploration. Particularly, after generating new proof states by executing the newly produced proof steps, we first invoke two complementary symbolic tools, QuickCheck [15] and Nitpick [14], to detect potential counterexamples in the can- didate states. QuickCheck performs random property-based testing on executable parts of the proof state, whereas Nitpick translates higher-order formulas into finite relational models and searches for counterexamples using Kodkod, which is a SAT-based first-order relational model finder. Additionally, we adapt the tool SolveDirect [29] to detect potentially duplicate proof states. Initially, SolveDirect deter- mines whether a newly stated theorem can be solved directly using an existing one. In our setting, we formalize two proof states as theorems and apply SolveDirect in both directions to determine whether they are semantically equivalent. We use a basic theorem in seL4 as an example to illustrate proof state filtering. Consider the āsigned overflowā theorem, whose formal statement is as follows. theorem sofl_test: ā¹ sint x + sint y = sint (x + y) āā drop_bit (size x - 1) ((x + y XOR x) AND (x + y XOR y)) = 0 āŗ for x y :: ā¹ āa::len word āŗ The theorem claims that for two signed machine words, the value of their machine-level sum matches the sum of the math- ematical values they represent. This property guarantees the correctness of the machine-word definitions on which the low-level kernel specifications depend. To prove this theorem, the LLM proposes a total of 8,445 candidate proof steps, ren- dering exhaustive exploration prohibitively time-consuming. Nevertheless, our filtering reveals that 44.2% of these steps lead to duplicate proof states, and 52.3% of the remaining states are unprovable due to existing counterexamples. Thus, the state-filtering process effectively eliminates unproductive effort and conserves the search budget, enabling the proof to be found much earlier. 3.2.2 Proof State Ranking To guide the proof search efficiently, we rank all proof states and always expand the most promising ones first. To score a given proof state, we rely on the log probabilities predicted by the fine-tuned LLM. The LLM is trained to predict the next proof step; its log probability directly reflects the modelās confidence in applying that step to the current proof state. Consider a candidate proof states L , obtained by apply- ing a sequence of proof steps(a 1 ,..., a Lā1 ). We define its cumulative log-probability score as score(s L ) = ā Lā1 t=0 log p(a t | s t ) L Ī± , wheres 1 ,..., s Lā1 are the intermediate states produced by the corresponding steps. The normalization termL Ī± mitigates the inherent bias against longer proof sequences, with the exponentĪ±specifying the degree of mitigation [18], which we set to 1 by default. After computing the score for each proof state, we select the top-k states for further expansion where k is a hyperparameter. 3.3 Hammer Integration Hammers are tools designed to discharge proof goals in ITPs automatically. In Isabelle, the primary hammer is Sledge- hammer [16], which applies ATPs and SMT solvers (e.g., Z3, CVC5, E, SPASS, Vampire, etc) to the current goal and syn- thesizes corresponding Isabelle proofs. When invoked, it first retrieves a fixed number of potentially relevant premises that 6 may aid in solving the goal. These premises, together with the goal, are translated into a form suitable for backend ATP and SMT solvers. If a backend solver succeeds, Sledgehammer attempts to reconstruct a corresponding Isabelle proof step, and, when this reconstruction succeeds, a complete proof for the current goal is returned to the prover. Although Sledgehammerās performance is far from satis- factory for our tasks, it plays a mutually beneficial role in the tree search process. In particular, while tree search may fail to solve the original problem within a limited search budget, it often reduces the problem to a simpler form that Sledge- hammer can solve, even though it cannot solve the initial goal on its own. This makes it natural to integrate the hammer into our framework. Because invoking the hammer at every search step is prohibitively expensive, we only call it when tree search fails. Specifically, upon search failure, we rank all proof states in the currently expanded tree, select a small sub- set with the highest scores, and pass them to Sledgehammer for a final attempt at solving the goal. 4 Evaluation This section presents our experimental results. We use seL4 as a system-level evaluation testbed to demonstrate both the effectiveness and efficiency of our proposed method. In ad- dition, we introduce four additional repository-level bench- marks to further assess its generalizability. Specifically, our study aims to address the following research questions (RQs): ā¢RQ1 ā Effectiveness: Does our proposed method outper- form existing techniques in generating proofs for seL4? ā¢RQ2 ā Efficiency: How much human effort in proving seL4 can be saved using our proposed method? ā¢RQ3 ā Generalizability: Can our method perform well on the verification of other software projects? ā¢ RQ4 ā Ablation: What is the contribution of each compo- nent within our framework? All evaluations were carried out within a dedicated Docker environment on a Linux server with an AMD EPYC 9654 96-core processor and six high-end GPUs. 4.1 Isabelle REPL To enable efficient interaction with Isabelle from Python, we implement a new Isabelle REPL (Read-Eval-Print Loop), 2 whose logic builds on scala-isabelle [30] and Py4J [31]. The 2 Isabelle REPL is an interactive command-line interface for the Isabelle theorem prover, designed to support incremental, exploratory proof develop- ment, which is similar in spirit to the REPLs found in programming languages such as Python, but adapted to Isabelleās document-oriented proof model. REPL provides a Gateway Server that exposes Isabelle com- ponents to Python clients through a unified API. This de- sign enables programmatic interaction with Isabelle, allowing users to parse Isabelle theories, extract run-time context infor- mation, and execute proof steps incrementally. Compared to the previously developed Isabelle REPL, PISA [32], our REPL supports more recent Isabelle versions and provides extended ML-level capabilities. A wide range of Isabelleās proof-automation tools, including Sledgehammer, Nitpick, Quickcheck, and other integrated methods, can be accessed directly through our interface. It also improves the extraction of information from proof contexts, such as vari- ables and assumptions in proof goals, dependencies of proved theorems, and facts selected by Sledgehammer. In addition, our REPL provides improved management of the Isabelle process, top-level state, and theories. It allows users to safely impose strict time limits on Isabelle processes, as well as to clone, restore, and switch between different proof states. Theory management is also strengthened: in large verification projects, complex theory dependencies can heavily degrade compilation efficiency. For example, in the CRefine theory of seL4, a single proof step takes more than one minute to process. To address this, we implement a caching mechanism that avoids redundant execution of unre- lated theorems and proofs, significantly reducing unnecessary recomputation. 4.2 Experimental Setup Dataset. We use the FVELER dataset [10], which comprises 29,125 theorems from seL4. The dataset is split into four sub- sets, i.e., training, validation, test, and test-hard, containing 26,081, 1,115, 1,077, and 852 theorems, respectively. Follow- ing the FVEL criteria, the training, validation, and test sets are randomly partitioned. In contrast, the test-hard set con- sists of theorems drawn from three specific and independent sessions, i.e., SysInit, SysInitExamples, and LibTest, that do not appear in any of the other splits. Note that sessions are the way Isabelle organizes theory files, which resemble the relationship between code files and libraries in other program- ming languages. A theory can import other theories, and a session can depend on other sessions by declaring dependen- cies in the Isabelle ROOT file. These sessions are typically selected based on the depth of their session-level dependency graphs, and the theorems they contain exhibit more complex dependencies, making them considerably more challenging to prove. In our experiments, we use the training set as the corpus for fine-tuning LLMs, and adopt validation, test, and test-hard sets to evaluate our proposed framework. From the training set, we further extract all proof stateāstep pairs, yielding a total of 181,887 pairs. On average, each theorem contributes to about seven pairs, substantially increasing the amount of supervised data available for model training. 7 Training. We fine-tuned two small models, Qwen3-1.7B [33] and Mistral-7B [12], to predict and score each proof step. We carried out the full-parameter supervised fine-tuning (SFT) using the Llama-Factory framework [34]. We use DeepSpeed ZeRO-2 optimization to enable memory-efficient distributed training. The training used an effective global batch size of 16 and ran 3 epochs using bfloat16 mixed precision. The learning rate was set to 1e-5 and followed a cosine decay schedule with a warmup ratio of 0.1. Proving. For the LLM inference, we adopt a high temperature of 1.0 and a top-p value of 0.95 to explore the proof space sufficiently. The maximum generation length is fixed at 2,048 tokens. In each search iteration, at most five proof states are selected; for each proof state, the model is prompted to generate 128 candidate proof steps. In our framework, we disable LLMsā internal thinking to improve inference efficiency. When proof search fails, we select the 16 highest-scoring proof states and invoke Sledgehammer for assistance. We run Sledgehammer with its default premise-selection strategy: it first selects 2,048 most relevant premises for the current proof goal using MeSh, which combines MePo [35] and MaSh [36] to gauge relevance between the proof goal and available facts in the context. With these retrieved results, Sledgehammer then attempts to discharge the current subgoal using the built- in SMT/ATP solvers Z3, CVC5, E, SPASS, and Vampire, with a 60s time limit. Baseline. We select four neural or symbolic proof-generation methods as baselines. Selene prompts GPT-4o with the tar- get problem and several examples to generate a candidate proof. FVEL follows a similar paradigm but also fine-tunes a Mistral 7B-Instruct model on the training data to produce complete proofs, rather than using in-context learning. We also include two symbolic methods, Auto and Sledgehammer, which operate purely symbolically to prove the target theorem. Here, Auto is a collection of common symbolic automatic proving methods in Isabelle, such asby simp,by auto, and by fastforce. The time limit for all methods is set to 120 minutes, as we observed no noticeable improvement when increasing it further. 4.3 Experimental Results 4.3.1 RQ1: Effectiveness Comparison Table 1 summarizes the performance of our approach com- pared to both neural and symbolic baselines. Among neural methods, Selene achieved 156 successful proofs, while FVEL improved this to 219. As for symbolic baselines, Auto proved 164 theorems, whereas Sledgehammer reached 1,124. In contrast, our framework substantially outperforms all these baselines across different splits. Using the fine-tuned Mistral- 7B model, our approach produces a total of 2,167 feasible proofs, of which 788 are on the validation set, 811 are on the Table 1: Proof success rates (%) across validation (Val), test (Test), and test-hard (TsHd) splits. Compared to existing neu- ral 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 base- line by 30.0% and 37.3%, respectively. METHODVALTESTTSHDTOTAL Neural Selene6.17.03.35.6 FVEL8.99.54.57.8 Symb. Auto 4.96.76.15.9 Hammer40.539.540.940.3 Ours Qwen373.674.961.170.4 āā33.1ā35.4ā20.2ā30.0 Mistral79.889.069.877.6 āā39.3ā49.5ā28.9ā37.3 test set, and 568 are on the test-hard set. This accounts for 77.6% of all still valid theorems across the three evaluated sets and proves 37.3% more theorems than the best baseline, Sledgehammer. It is also encouraging that, on a relatively small model, Qwen3-1.7B, our approach manages to com- plete the proof of 1,965 theorems, which amounts to 70.4% of the total theorems. This demonstrates that in a real environ- ment where new proofs need to be crafted, a deployed small model can already help with the development of verification. We further evaluate the performance of our automated prov- ing approach in two aspects. First, prior work has struggled with generating nontrivial proofs. Since the proofs in seL4 are largely procedural, we use the proof length as a proxy for proving difficulty. We compute the proof success rate across different proof lengths and present the results in Figure 3. The results show that our approach is more capable of prov- ing longer theorems than previous baselines. Although the success rate naturally decreases as proof length increases, it remains around 20% even for the 393 theorems whose proofs exceed 10 lines. We leave it as future work to investigate more effective strategies for constructing longer proofs. Second, we examine the performance across different proof sessions. We group the seL4 theorems into six major cate- gories w.r.t. the functionality [5,37,38]: Base Libraries & Tools (Base), Specifications (Spec), Abstract-Level (A-Level) Properties, Refinement from Abstract-Level to Executable C (AāC), Security/Information Flow Control (IFC), and Sys- tem Initialization Group (SysInitGroup). Figure 4 presents the results across these categories, demonstrating that our approach delivers superior performance compared with all baselines across all sessions. Notably, under the test-hard set division strategy, SysInitGroup is derived from a completely distinct session and is isolated from the training data, yet our approach still achieves a success rate of 67.6%. 8 12345678910>10 Ground-truth Proof Length 0 20 40 60 80 100 Proof Success Rate (%) Selene Auto Ours (Qwen) FVEL Hammer Ours (Mistral) 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. Table 2: Coverage results of automatically generated proof lines. Our method attains the highest coverage, proving theo- rems whose existing proofs amount to over one-third of all proof lines and substantially outperforming existing baselines in reducing manual proof-script development effort. METHOD# OF PROOF LINES% OF COVERAGE Selene1971.1 FVEL2711.6 Auto 2041.2 Hammer 2,58115.0 Ours6,23536.2 Response to RQ1 Our approach substantially outperforms baselines, producing 37.3% more proofs than the (symbolic) ATP tool Sledgehammer and 69.8% more proofs than the state-of-the-art neural method. It remains reliably effective across different proof difficulty levels and session categories. Further, it demonstrates good gen- eralizability, successfully discharging 67.6% of the theorems from unseen sessions during training. 4.3.2RQ2: Proving Efficiency in Saving Human Efforts To evaluate how effectively our approach reduces manual effort in developing proof scripts, we adopt a standard met- ric: the coverage of the entire library that can be automati- cally generated [39]. As summarized in Table 2, our method successfully proves theorems whose corresponding proofs account for 6,235 lines in the seL4 proof corpus, achieving 36.2% coverage across all evaluated theorems. Under this metric, our approach yields more than a one-fold improve- ment over existing baseline methods. Base Spec A-Level Properties Refinement (AC) Security / IFCSysInitGroup 20% 40% 60% 80% Selene Hammer FVEL Ours (Qwen) Auto Ours (Mistral) Figure 4: Proof success rates across the six seL4 session cat- egories. Our approach yields stronger performance than all baselines in all sessions. Notably, it achieves high accuracy even on the challenging SysInitGroup category, which is en- tirely unseen during training. 0%10%20%30%40%50%60%70%80%90% Expert-written Proof Ratio 70 80 90 Pass Rate (%) 77.61 77.65 77.87 78.01 78.40 79.23 79.76 80.73 82.74 86.03 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. We further situate our method within an AIāhuman collab- orative pipeline to evaluate its efficiency in reducing human effort. Specifically, for each theorem, we provide a portion of the ground-truth proof lines (simulating human expert-written proof) and ask our approach to complete the remaining steps. Figure 5 shows the proof completion rate curve w.r.t. the proportion of ground-truth proof. As expected, supplying more expert-written proof lines enables our method to complete more theorems. Ultimately, including cases solved entirely automatically, our approach succeeds in automatically completing at least 10% export ef- fort for 86.0% of the theorems. We then calculate the average effort saving (AES) of our approach: AES = p 1 Ļ 1 + k ā i=2 (p k ā p kā1 )Ļ k , 9 where(Ļ 1 ,..., Ļ k )are the ratios of expert-written proof lines in ascending order, with the corresponding proof completion rates are(p 1 ,..., p k ). Therefore, under this AIāhuman col- laboration setting, the automated proof completion reduces human effort by an average of 71.1%. We also record the time consumption of our framework as a reference; the average time to generate a successful proof is 139.1 minutes. However, it is worth noting that this average is skewed upward by a small number of theorems that take extremely long to prove. In our experiment, we find that 58.4% of the theorems are proved within 10 minutes, 73.4% within 30 minutes, and 80.8% within 2 hours. Therefore, the majority of proofs are obtained within a relatively short time horizon, indicating that our framework is generally highly efficient despite a few outliers with long proof times. Response to RQ2 Our approach alleviates much of the burden of in- teractive theorem proving, automatically completing proofs that correspond to 36.2% of the proof lines in the evaluated corpus and reducing expert effort by approximately 71.1% in an AIāhuman collaboration setting. Moreover, it is able to synthesize the majority of proofs within a practical time budget. 4.3.3 RQ3: Generalizability to Other Projects A major concern with training-based methods is their gener- azability, namely, whether the approach is only applicable to a specific domain due to potential data leakage or overfitting. To investigate possible leakage, given that the seL4 proofs are publicly available and that the pre-trained model may have already incorporated some of the knowledge, we compute the similarity between the ground-truth proofs and the proofs gen- erated by our approach. We adopt sequence similarity [40] and Jaccard similarity [41] as the evaluation metrics. The re- sults are shown in Figure 6. They indicate that both similarity scores remain low except for one- or two-line proofs, which is not surprising since very short proofs tend to be identical. We further examined these short proofs and found that only 16.7% are identical, providing strong evidence that data leakage in our fine-tuned model is unlikely. We further explore the generalizability of our approach and the fine-tuned LLM. We select three projects from the Archive of Formal Proofs (AFP 3 ), i.e., X86 Semantics [42], IEEE Floating Point [43], and SATSolverVerification [44], to directly apply proof search on the theorems therein. In addi- tion, we include the code verification benchmark Code2Inv and translate its loop invariants into Isabelle theorems. The performance of our approach and baselines is shown in Figure 7. Because the X86 semantics benchmark is more 3 http://afp.sf.org 12345678910>10 Ground-truth Proof Length 0.0 0.2 0.4 0.6 0.8 1.0 Similarity Sequence Similarity Jaccard Similarity Figure 6: Sequence and Jaccard similarity between gener- ated and ground-truth proofs. (Note that sequence similarity measures how alike two ordered sequences are based on their matching elements and positions, while Jaccard similarity measures how similar two sets are by comparing the propor- tion of shared elements to the total distinct elements.) Both similarities stay below the thresholds of indicating potential data leakage across different proof lengths. relevant to the seL4 project, the fine-tuned LLM performs particularly well on it, yielding a 32.5% higher success rate than the baselines. The other three benchmarks are hammer- friendly because of their SMT-oriented nature. Even in this setting, our framework demonstrates superior effectiveness, achieving an average relative improvement of 36.9%. Response to RQ3 The knowledge acquired by the fine-tuned LLM, to- gether with our proof search framework, generalizes well across domains. In particular, the approach can be effectively leveraged to assist proof construction in a wide range of formal verification tasks beyond the seL4 setting. 4.3.4 RQ4: Ablation study Since our approach integrates several components, namely LLMs, hammer, as well as proof-step revision and proof-state filtering mechanisms, we conduct ablation studies to evaluate the contribution of each part of the framework. To assess the impact of our fine-tuned model, we replace it with off-the- shelf LLMs such as GPT-4o or DeepSeek. Due to budget constraints (running tree search for a single problem costs ap- proximately $4.1 when using the DeepSeek or GPT-4o APIs), we randomly sample 200 theorems from the benchmark and use the DeepSeek API to propose proof steps. In addition, inspired by Rango [8], we implement a retrieval-augmented generation (RAG) mechanism. The re- trieval module fetches both similar proof steps and potentially relevant premises. Similar steps are retrieved from the train- ing set based on the similarity between their associated proof states and the current proof state, where these states are tok- enized into sequences of identifiers, and relevance is measured using BM25 [45]. For premises retrieval, we continue to rely 10 X86 Semantics (86) IEEE Floating Point (188) SATSolverVerification (564) Code2Inv* (399) 0 20 40 60 80 Proof Success Rate (%) 2.3 1.1 3.5 0.0 14.0 6.9 2.7 0.0 10.5 10.6 1.2 12.5 32.6 48.4 48.0 12.8 65.1 58.0 55.1 22.6 Selene Auto Ours (Mistral) FVEL Hammer Figure 7: Performance of our proof search framework on ad- ditional benchmarks. Thex-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. on Sledgehammerās MePo heuristic for efficiency. The final prompt for LLMs includes the retrieved steps and premises along with their statements, and we restrict the total lengths of steps and premises to 1024 and 512 tokens, respectively. The results for all method variations are reported in Ta- ble 3. Overall, although adding tree search and RAG steadily improves DeepSeekās performance, these variants still fall significantly short of our full framework. This confirms that the combination of the fine-tuned model, structured search, and hammer integration is essential for achieving high proof success rates, and highlights the importance of each major component in our design. To evaluate the impact of the step revision mechanism, we analyze the theorems that become difficult to prove when the revision is disabled. We observe that revision is most beneficial when the LLM fails to generate enough effective proof steps. In particular, for the most challenging 77 theo- rems where the model initially proposed no valid steps and therefore failed immediately, the revision procedure is highly effective, enabling 24.7% of these theorems to be proved. For a broader set of 220 theorems where the LLM proposed fewer than 5% valid steps, the revision mechanism still provides substantial gains, allowing 11.8% of them to succeed. Regarding the necessity of proof state filtering, particularly the counterexample detection, our experiments show that in- corporating this component allows the system to identify an average of 1.3 counterexamples per evaluated theorem. For the subset of search traces that contain counterexamples, the average number rises to 11.1. These results indicate that coun- terexample detection is valuable for identifying unprovable 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 in- corporated, 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 sub- stantially stronger performance. METHOD VARIATIONRATE DeepSeek (DpSk) v3.25.5 DpSk + Tree Search12.5 DpSk + RAG + Tree Search 33.0 DpSk + RAG + Tree Search + Hammer52.0 Ours (Trained LLM + Tree Search + Hammer)70.0 states early and preventing unproductive search efforts, al- though it does not directly increase the overall proof success rate. Response to RQ4 Each of the symbolic and neural components in our framework plays an essential role, and their synergy substantially strengthens the overall theorem-proving capability for software verification. 5 Related Work 5.1 Software System Verification via ITP Formal methods have successfully verified critical software systems including operating system kernels, hypervisors, file systems and compilers. Interactive theorem proving (ITP) pro- vides strong formal assurance by allowing engineers to encode specifications and build proofs in ITP systems such as Rocq or Isabelle/HOL. Notable examples include CertiKOS [46], which employs a compositional refinement framework to ver- ify a layered OS kernel; CompCert [4], an optimizing C compiler whose translation passes are all verified to preserve semantics; FSCQ [11], a crash-safe file system proven correct under all failure scenarios using Crash Hoare Logic; seKVM hypervisor [47], a reduced KVM core with enforced con- fidentiality and integrity of guest memory; seL4 [5], an OS microkernel which remains the most comprehensive and influ- ential milestone for formal system verification. These efforts demonstrate that ITP enables high-assurance proofs for criti- cal systems, albeit at a significant engineering cost. 11 5.2 Automated Theorem Proving Automated theorem proving (ATP) has long served as a bench- mark for machine reasoning. Classical ATP systems rely on symbolic methods, such as resolution-based first-order provers (e.g., Vampire [48], E [49]) and SMT solvers (e.g., Z3 [50], CVC5 [51]) with built-in theories. These solvers are also integrated into interactive theorem provers via hammers (e.g., Sledgehammer [16] in Isabelle), enabling automated discharge of proof goals [52]. Related to ATP, several works (e.g., Ironclad Apps [53] and Verve [54]) leverage verification- aware languages (e.g., Dafny [55] and Boogie [56]) to prove memory and control-flow safety of system components, in- cluding kernels and device drivers. In recent years, machine learning has been increasingly applied to ATP. Early efforts focused on premise selec- tion and tactic prediction using classical learning methods (e.g., Holophrasm [57], TacticToe [27], Proverbot9001 [58], Diva [59]), showing improved success rates in Metamath, HOL4, and Coq. More recently, large language models (LLMs) have been utilized to generate complete proofs or sketches [60,61], achieving possible superhuman results on mathematical problems [62]. Prior attempts to extend these capabilities to software verification include Baldur [63], PALM [64], and Guided Proof Search [65]. However, they remain limited to textbook-scale problems, which are insuf- ficient to address challenges from real-world systems-level verification projects such as seL4. Complementary to whole-proof generation, the proof-step prediction paradigm harnesses LLMs to propose the next tac- tic or lemma, guided by proof-state feedback. Systems such as GPT-f [66], LISA [32], HTPS [67] and LeanDojo [21] demon- strate the potential of this class of methods across Metamath, Isabelle and Lean. However, this line of work primarily tar- gets singleton mathematical problems and therefore does not scale to system-level software verification. Our method fills this gap by integrating a fine-tuned LLM for proof search with symbolic techniques, specifically, proof-step revision and proof-state filtering, making large-scale verification both effective and efficient. To further enhance reliability, hybrid approaches are pro- posed to incorporate symbolic provers into LLM pipelines. A series of works, e.g., Thor [68], ProofAug [69] and Strat2Rocq [70], exemplify this by coupling LLM-generated reasoning with ATPs or hammers. Yet, ATP-based verification fundamentally trades expressiveness for automation, limiting scalability in system-level contexts. In contrast, our method integrates LLMs with an ITP workflow, invoking ATPs only in the final stage to discharge the remaining proof obligations. 6 Limitations and Future Work Despite strong empirical performance, our framework has several limitations that suggest directions for future research. Computational cost. The overall tree-search procedure re- mains computationally expensive. Each iteration requires invoking Isabelle for proof-step execution and proof-state checking, which results in substantial runtime overhead. Fu- ture work includes developing efficient state caching, parallel expansion, and cost-aware search policies to minimize unnec- essary exploration and improve throughput. Performance degradation for longer proofs.While our method successfully constructs longer proofs than prior meth- ods, its performance indeed degrades as proof length in- creases. The current tree-search procedure adopts one-step prediction and bounded search, making it challenging to un- cover deeper reasoning chains. Future improvements could involve hierarchical planning, subgoal decomposition, or re- inforcement learning from bootstrapped trajectories. Rigid rule-driven step revision. The proof step revision mod- ules heavily rely on heuristic tactic-premise recombination and lightweight premise retrieval. These mechanisms, though helpful, are imperfect and may introduce misleading candi- dates. Future improvements may include learning the rele- vance of premises directly from the proof state or integrating stronger semantic filters. 7 Conclusion In this paper, we have presented a neuro-symbolic proof- generation framework that automates proof search for large- scale software verification projects in interactive theorem provers. Instead of attempting whole-proof synthesis, our approach performs a best-first tree search over fine-grained proof states, repeatedly querying a lightweight, fine-tuned LLM for the next proof step. This paradigm not only substan- tially improves data efficiency, but also enables a seamless integration of symbolic reasoning tools with LLM-based step generation and scoring, forming an effective and efficient pipeline for proof-step construction as well as proof-state filtering and ranking. The experiments on the seL4 verifica- tion corpus show our approach significantly outperform prior baselines. Notably, our method succeeds on a considerably higher proportion of multi-step, nontrivial theorems, address- ing a long-standing limitation of LLM-based provers. Addi- tional experiments on AFP projects and translated program- verification benchmarks further showcase strong cross-project generalizability. Our work provides compelling evidence that proof- stepācentric neuro-symbolic search can serve as a practical path toward scalable and automated software verification at the systems level, e.g. operating systems kernels, network architecture, and databases. Although there is still a long way to go, we are making promising progress towards develop- ing AI-enabled, rigorous engineering methods for real-world computer systems. Availability 12 The tool and all experimental data are available at the fol- lowing private link, 4 and a prebuilt Docker image containing the seL4 verification environment and all required dependen- cies will also be released. 4 https://figshare.com/s/da4d1d995a9a64eeadf? file=60276236 13 References [1]Edmund M. Clarke and Jeannette M. Wing. Formal methods: state of the art and future directions. ACM Computing Surveys, 28(4):626ā643, 1996. [2]Bruno Blanchet, Patrick Cousot, Radhia Cousot, JĆ©rĆ“me Feret, Laurent Mauborgne, Antoine MinĆ©, David Mon- niaux, and Xavier Rival. A static analyzer for large safety-critical software. In Proceedings of the ACM SIGPLAN Conference on Programming Language De- sign and Implementation (PLDI), pages 196ā207, 2003. [3]James Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John Fitzgerald. Formal methods: Practice and ex- perience. ACM Computing Surveys, 41(4):1ā36, 2009. [4] Xavier Leroy, Sandrine Blazy, Daniel KƤstner, Bern- hard Schommer, Markus Pister, and Christian Ferdinand. Compcert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, 2016. [5]Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Ger- not Heiser. Comprehensive formal verification of an os microkernel. ACM Transactions on Computer Systems (TOCS), 32(1):1ā70, 2014. [6]Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Glig- oric, Zachary Tatlock, et al. Qed at large: A survey of engineering of formally verified software. Foundations and TrendsĀ® in Programming Languages, 5(2-3):102ā 281, 2019. [7]Jianxing Qin, Alexander Du, Danfeng Zhang, Matthew Lentz, and Danyang Zhuo. Can large language models verify system software? a case study using fscq as a benchmark. In Proceedings of the 2025 Workshop on Hot Topics in Operating Systems, pages 34ā41, 2025. [8]Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern, Yuriy Brun, JoĆ£o F Fer- reira, Sorin Lerner, and Emily First. Rango: Adaptive retrieval-augmented proving for automated software ver- ification. In 2025 IEEE/ACM 47th International Confer- ence on Software Engineering (ICSE), pages 347ā359, 2025. [9]Lichen Zhang, Shuai Lu, and Nan Duan. Selene: Pio- neering automated proof in software verification. In Pro- ceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (ACL), pages 1776ā1789, 2024. [10] Xiaohan Lin, Qingxing Cao, Yinya Huang, Haiming Wang, Jianqiao Lu, Zhengying Liu, Linqi Song, and Xiaodan Liang. Fvel: Interactive formal verification environment with large language models via theorem proving. Advances in Neural Information Processing Systems, 37:54932ā54946, 2024. [11]Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chli- pala, M Frans Kaashoek, and Nickolai Zeldovich. Using crash hoare logic for certifying the fscq file system. In Proceedings of the 25th Symposium on Operating Sys- tems Principles, pages 18ā37, 2015. [12]Albert Q. Jiang, Alexandre Sablayrolles, Arthur Men- sch, Chris Bamford, Devendra Singh Chaplot, Diego de las Casas, Florian Bressand, Gianna Lengyel, Guil- laume Lample, Lucile Saulnier, LĆ©lio Renard Lavaud, Marie-Anne Lachaux, Pierre Stock, Teven Le Scao, Thibaut Lavril, Thomas Wang, TimothĆ©e Lacroix, and William El Sayed.Mistral 7b.arXiv preprint arXiv:2310.06825, 2023. [13]Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The llama 3 herd of models. arXiv e-prints, pages arXivā2407, 2024. [14]Jasmin Christian Blanchette and Tobias Nipkow. Nit- pick: A counterexample generator for higher-order logic based on a relational model finder. In International con- ference on interactive theorem proving, pages 131ā146. Springer, 2010. [15]Koen Claessen and John Hughes.Quickcheck: a lightweight tool for random testing of haskell programs. In Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, pages 268ā279, 2000. [16] Sascha Bƶhme and Tobias Nipkow. Sledgehammer: judgement day. In International Joint Conference on Automated Reasoning, pages 107ā121. Springer, 2010. [17]Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024. [18] Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for llm- based automatic theorem proving.arXiv preprint arXiv:2502.03438, 2025. [19]Google DeepMind. Gemini: A family of highly capable multimodal models.https://deepmind.google/ technologies/gemini/, 2024. Accessed model vari- ant: Gemini 3 Pro. 14 [20]OpenAI.Gpt-4 technical report.arXiv preprint arXiv:2303.08774, 2024. [21]Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chala- mala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: The- orem proving with retrieval-augmented language mod- els. Advances in Neural Information Processing Sys- tems, 36:21573ā21612, 2023. [22] Ian Berlot-Attwell, Frank Rudzicz, and Xujie Si. Llm library learning fails: A lego-prover case study. arXiv preprint arXiv:2504.03048, 2025. [23]Tobias Sesterhenn, Ian Berlot-Attwell, Janis Zenkner, and Christian Bartelt. A compute-matched re-evaluation of trove on math. arXiv preprint arXiv:2507.22069, 2025. [24]Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. Tacticzero: Learning to prove theo- rems from scratch with deep reinforcement learning. Advances in Neural Information Processing Systems, 34:9330ā9342, 2021. [25]Suozhi Huang, Peiyang Song, Robert Joseph George, and Anima Anandkumar. Leanprogress: Guiding search for neural theorem proving via proof progress prediction. arXiv preprint arXiv:2502.17925, 2025. [26]Yuhuai Wu, Albert Jiang, Roger Grosse, and Jimmy Ba. Neural theorem proving on inequality problems. Artifi- cial Intelligence and Theorem Proving (AITP), 2020. [27] Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ra- mana Kumar, and Michael Norrish. Tactictoe: learning to prove with tactics. Journal of Automated Reasoning, 65(2):257ā286, 2021. [28]Bartosz Piotrowski, Ramon FernĆ”ndez Mir, and Edward Ayers. Machine-learned premise selection for lean. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 175ā186. Springer, 2023. [29] Timothy Bourke and Gerwin Klein. Solve_direct: A tool for isabelle/hol to check whether a newly stated theorem can be solved directly by an existing theorem. https://isabelle.in.tum.de/library/HOL/ HOL/ISABELLE_HOME/src/Tools/solve_direct. ML.html , 2025. File: src/Tools/solve_direct.ML in Isabelle/HOL library. [30]Dominique Unruh.scala-isabelle: A scala library for interacting with isabelle.https://github.com/ dominique-unruh/scala-isabelle, 2025.Ac- cessed 2025-11-18. [31]N. M. Nishant and G. S. Mamatha. Using py4j for java-python communication. International Journal of Advanced Research in Computer and Communication Engineering (IJARCCE), 2023. [32]Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pages 378ā392, 2021. [33] An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chen- gen Huang, Chenxu Lv, et al. Qwen3 technical report. arXiv preprint arXiv:2505.09388, 2025. [34]Yaowei Zheng, Richong Zhang, Junhao Zhang, Yanhan Ye, Zheyan Luo, Zhangchi Feng, and Yongqiang Ma. Llamafactory: Unified efficient fine-tuning of 100+ lan- guage models. In Proceedings of the 62nd Annual Meet- ing of the Association for Computational Linguistics (Volume 3: System Demonstrations), Bangkok, Thai- land, 2024. Association for Computational Linguistics. [35]Jia Meng and Lawrence C Paulson. Lightweight rele- vance filtering for machine-generated resolution prob- lems. Journal of Applied Logic, 7(1):41ā57, 2009. [36]Daniel KĆ¼hlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. Mash: machine learning for sledgehammer.In International Conference on Interactive Theorem Proving, pages 35ā50. Springer, 2013. [37]Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick, and Gerwin Klein.seL4 enforces integrity. In Proceedings of the Second Inter- national Conference on Interactive Theorem Proving, ITP ā11, pages 325ā340, Berlin, Heidelberg, August 2011. Springer-Verlag. [38]Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. seL4: From general pur- pose to a proof of information flow enforcement. In IEEE Symposium on Security and Privacy, pages 415ā 429, San Francisco, CA, May 2013. IEEE. [39]Daniel Matichuk, Toby Murray, June Andronick, Ross Jeffery, Gerwin Klein, and Mark Staples. Empirical study towards a leading indicator for cost of formal soft- ware verification. In Proceedings of the 37th Interna- tional Conference on Software Engineering - Volume 1, ICSE ā15, page 722ā732. IEEE Press, 2015. [40]VI Lcvenshtcin. Binary coors capable or ācorrecting deletions, insertions, and reversals. In Soviet physics- doklady, volume 10, 1966. 15 [41]Paul Jaccard.Ćtude comparative de la distribution florale dans une portion des alpes et des jura. Bull Soc Vaudoise Sci Nat, 37:547ā579, 1901. [42] Freek Verbeek, Abhijith Bharadwaj, Joshua Bock- enek, Ian Roessle, Timmy Weerwag, and Binoy Ravin- dran. X86 instruction semantics and basic block sym- bolic execution.Archive of Formal Proofs, Octo- ber 2021.https://isa-afp.org/entries/X86_ Semantics.html, Formal proof development. [43] Lei Yu.A formal model of ieee floating point arithmetic.Archive of Formal Proofs, July 2013.https://isa-afp.org/entries/IEEE_ Floating_Point.html, Formal proof development. [44]Filip Mari Ģ c.Formal verification of mod- ern sat solvers.Archive of Formal Proofs, July 2008.https://isa-afp.org/entries/ SATSolverVerification.html, Formal proof devel- opment. [45]Stephen Robertson, Hugo Zaragoza, et al. The proba- bilistic relevance framework: Bm25 and beyond. Foun- dations and TrendsĀ® in Information Retrieval, 3(4):333ā 389, 2009. [46]Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan New- man Wu, Jieung Kim, Vilhelm Sjƶberg, and David Costanzo.CertiKOS: An extensible architecture for building certified concurrentOSkernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), pages 653ā669, 2016. [47]Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. Formally verified memory protection for a commodity multiprocessor hypervisor. In 30th USENIX Security Symposium (USENIX Security 21), pages 3953ā3970. USENIX Association, August 2021. [48]Alexandre Riazanov and Andrei Voronkov. The design and implementation of vampire. AI communications, 15(2-3):91ā110, 2002. [49] Stephan Schulz, Simon Cruanes, and Petar Vukmirovi Ģ c. Faster, higher, stronger: E 2.3. In International Confer- ence on Automated Deduction, pages 495ā507. Springer, 2019. [50] Leonardo De Moura and Nikolaj BjĆørner.Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337ā340. Springer, 2008. [51]Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nƶtzli, et al. cvc5: A versatile and industrial-strength smt solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 415ā442. Springer, 2022. [52]Åukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. Journal of auto- mated reasoning, 61(1):423ā453, 2018. [53]Chris Hawblitzel, Jon Howell, Jacob R Lorch, Ar- jun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill.Ironclad apps:End-to-Endsecurity via auto- matedFull-Systemverification. In 11th USENIX symposium on operating systems design and implemen- tation (OSDI 14), pages 165ā181, 2014. [54]Jean Yang and Chris Hawblitzel. Safe to the last instruc- tion: automated verification of a type-safe operating system. Communications of the ACM, 54(12):123ā131, 2011. [55]K Rustan M Leino. Dafny: An automatic program verifier for functional correctness. In International con- ference on logic for programming artificial intelligence and reasoning, pages 348ā370. Springer, 2010. [56]Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K Rustan M Leino. Boogie: A mod- ular reusable verifier for object-oriented programs. In International Symposium on Formal Methods for Com- ponents and Objects, pages 364ā387. Springer, 2005. [57]Daniel Whalen. Holophrasm: a neural automated the- orem prover for higher-order logic.arXiv preprint arXiv:1608.02644, 2016. [58]Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. Generating correctness proofs with neural networks. In Proceedings of the 4th ACM SIG- PLAN International Workshop on Machine Learning and Programming Languages, pages 1ā10, 2020. [59] Emily First and Yuriy Brun. Diversity-driven automated formal verification. In Proceedings of the 44th Inter- national Conference on Software Engineering, pages 749ā761, 2022. [60]Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Timo- thee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations (ICLR), 2023. [61]Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, and Fan Yang. Reviving dsp for advanced theorem proving in the era of reasoning models. arXiv preprint arXiv:2506.11487, 2025. 16 [62]Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625(7995):476ā482, 2024. [63] Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 1229ā1241, 2023. [64]Minghai Lu, Benjamin Delaware, and Tianyi Zhang. Proof automation with large language models. In Pro- ceedings of the 39th IEEE/ACM International Confer- ence on Automated Software Engineering, pages 1509ā 1520, 2024. [65] Tarun Prasad and Nada Amin. Guided proof search using large language models and lemma extraction in coq. In ICLR 2025 Workshop: VerifAI: AI Verification in the Wild, 2024. [66]Stanislas Polu and Ilya Sutskever.Generative lan- guage modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. [67]Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337ā 26349, 2022. [68]Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz OdrzygĆ³ Ģzd Ģz, Piotr MiÅo Ģ s, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding ham- mers to integrate language models and automated theo- rem provers. Advances in Neural Information Process- ing Systems, 35:8360ā8373, 2022. [69] Haoxiong Liu, Jiacheng Sun, Zhenguo Li, and An- drew C Yao. Proofaug: Efficient neural theorem proving via fine-grained proof structure analysis. arXiv preprint arXiv:2501.18310, 2025. [70]Jian Fang, Yican Sun, and Yingfei Xiong. Proof strategy extraction from llms for enhancing symbolic provers. arXiv preprint arXiv:2510.10131, 2025. 17