Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; rechecked every number, fraction and percentage (Tables 2 to 4, budget curves, RQ3 and RQ4 figures, training settings), page references, quotations, technique steps and the Verus sketches; changed one claim (the one proof in four reading of the 84 wrong done rationales was widened); Verus loop sketch checked against the Verus reference only by reading, not run.

source: Jianyu Zhang, Fuyuan Zhang, Jiayi Lu, Jilin Hu, Xiaoyi Yin, Long Zhang, Feng Yang, Yongwang Zhao, arXiv:2602.08384v1 (9 Feb 2026), 30 pages with appendices A to D. Pages cited are the printed page numbers. The method is called AutoReal and the model AutoReal-Prover.

earlier note: topic_studies/formal_verification_rust/llm_for_verification/c_and_systems_proofs.md has a six-line entry (method in one line, the 51.67% figure, the hold-out caveat). It has no steps, no prompts, no per-category numbers, no account of the context oracle, and no Verus form. Those are what this study adds.

the result and its biggest condition

A 7B open model (Qwen2.5-Coder-7B), fine-tuned on seL4 proofs in which every proof command is followed by a comment explaining it, writes whole Isabelle proofs in one generation. Given 256 tries per theorem it proves 341 of 660 seL4 theorems (51.67%) and 243 of 451 theorems in three AFP projects (53.88%).

The condition: the model is handed exactly the definitions and lemmas that the human proof used. “In our evaluation, the proof context supplied to AutoReal-Prover is kept consistent with the definitions and lemmas used in the corresponding human-written proofs [3,2].” (§3.4, p.12) So the numbers measure proof writing with the premises already chosen by an oracle. The paper states the gap in its last paragraph: “At the same time, while AutoReal closely follows existing verification practice, the extraction of theorem-relevant proof context is not yet automated and currently requires human input.” (§6, p.19)

proved, measured, trusted

Proved: nothing new about seL4. Every counted proof is checked by Isabelle against an unchanged theorem statement, since the method replaces only the proof body: “we replace the original human-written proofs with proofs generated by AutoReal-Prover in the corresponding theories and check them using the Isabelle proof checker” (§4.1, p.13).

Measured: proof success rate under an attempt budget (Tables 2 and 3), rationale accuracy (RQ3), difference from human proofs (RQ4), an ablation on 105 theorems (Table 4).

Trusted or unexamined: the theorem statements (taken from seL4 and AFP); the hand-supplied context; the quality of the roughly 200k training rationales, which were written by an untuned 7B model and never checked; who judged the RQ3 rationales and by what rubric (not stated).

technique 1: step-level rationale data from proof traces

What it is. For every proof step in an existing corpus, generate a short explanation of what the step does to the proof state, using the recorded state before and after as evidence.

When to use. When a project already has many machine-checked proofs and a tool that can replay them step by step and print the goals.

How it is done (§3.2, pp.7-9).

1. Get traces. The paper takes them from FVELER, “which records seL4 proof developments as sequences of individual proof steps together with their corresponding Isabelle proof states” (§3.2, p.7).
2. Hold out the test set first. “To prevent information leakage during evaluation, we adopt a strict hold-out protocol: proof steps associated with the theorems used for evaluation are excluded from CoT data construction and reserved for testing.” (§3.2, p.8)
3. Build one input per step. “For each proof step, we construct a structured input for CoT generation that combines four components: (1) the source lemma, including its identifier and statement; (2) the proof state before applying the step, including the current subgoals; (3) the proof step itself, namely the Isabelle command to be explained; and (4) the proof state after applying the step.” (§3.2, p.8)
4. Ask a model to explain. The prompt (Fig. 8, Appendix A.2, p.24) opens: “You are analyzing a single proof step from the seL4 Isabelle verification project.” It then asks for the reasoning of this single step, forbids restating the input, and demands one concise paragraph in a technical third-person style.
5. The generator is Qwen2.5-Coder-7B, the same base model that is later fine-tuned (§3.2, p.8).
6. Collect about 200k instances. “Each instance pairs a single proof step with a natural-language explanation describing (1) the proof methods, lemmas, and definitions applied in the step and their purpose; (2) the resulting change to the proof state, such as simplifying or discharging subgoals; and (3) the contribution of the step to the overall progress of the proof.” (§3.2, p.9)

The paper’s example (Fig. 9, Appendix B.1, p.24): lemma power_2_mult_step_le, step apply (cases "n' = n", simp), state before with 1 subgoal, state after with 2 subgoals, and a rationale saying the step splits on whether n' equals n and simplifies the first case.

Verus form. Inference: Verus has no tactic steps and prints no goal list, so the four-part input does not exist as such. The nearest unit is one proof annotation: a loop invariant clause, an assert, an assert ... by block, or a call to a lemma proof fn. The nearest “state before and after” is the verifier’s error list without and with that annotation, obtained by deleting it and re-running Verus. A rationale then says which failing obligation the annotation discharges. What does not carry over: in Isabelle each step provably changes the state, while a Verus annotation may be redundant (removing it changes nothing), so a share of annotations would have no evidence to explain.

Evidence. Only indirect, through the ablation in technique 2. The rationales in the training data were not audited.

Where it fails. The explanation is produced by a small general model that sees only one step; nothing checks it. Fig. 9’s rationale says the second case assumes n’ < n where the printed state has n’ ≠ n together with n’ ≤ n, a harmless slip here but a sign that rationales are approximate.

technique 2: train to emit proof commands interleaved with rationales, in one pass

What it is. Fine-tune so that the output is the whole proof, each command followed by its explanation as a comment. The claim is that the explanations make the model track the proof state by itself: “As a result, step-aligned explanations can stand in for explicit proof-state queries, enabling proof generation in a single inference without repeated interaction with Isabelle.” (§3.3, p.10)

When to use. When calling the checker after every step is too slow, and one whole-proof check per attempt is affordable.

How it is done (§3.3, pp.9-11; Appendix C, p.28).

1. Training input: “The training input consists of the target lemma together with its associated proof context, while the training output is a single structured sequence that alternates between Isabelle proof commands and step-aligned reasoning explanations derived from the step-level proof CoT data constructed in Section 3.2.” (§3.3, p.10)
2. Output shape, from Fig. 5 (p.10):

whole proof:
apply (unfold setEndpoint_def)
(* The proof step unfolds the definition of `setEndpoint`, simplifying the goal ... *)
apply (rule setObject_ep_pre)
(* The proof step applies the `setObject_ep_pre` rule, strengthening the precondition ... *)
...
done
(* The proof completes successfully with no remaining subgoals ... *)

3. Fine-tune Qwen2.5-Coder-7B by instruction tuning (§3.3, pp.10-11).
4. Settings: “Training is performed in bf16 precision with a maximum sequence length of 8192.” (Appendix C, p.28) Per-device batch 1 with gradient accumulation 32, 10 epochs, cosine schedule with warmup ratio 0.03, learning rate 5 × 10⁻⁶, weight decay 0.05, gradient norm cap 0.3, paged AdamW 8-bit.
5. At inference, use the fixed prompt (Fig. 7, Appendix A.1, p.23): “You are an Isabelle proof expert, and I need you to help me prove the theorems in the project and explain the reasoning behind each proof step.” The prompt goes on to say the lemma and context will be given and that each step must be followed by its chain of thought.

Not in the paper: how many whole-proof training instances there are, how the per-step rationales are joined into them, the hardware, the training time, the sampling temperature.

Verus form. Inference: the same output shape is a Verus function body in which each proof annotation carries a comment naming the obligation it serves.

verus! {
// sketch, not machine-checked
fn count_up(n: u32) -> (r: u32)
    ensures r == n,
{
    let mut i: u32 = 0;
    while i < n
        invariant
            // keeps i in range, so i + 1 cannot overflow; with the exit
            // condition i >= n it gives the postcondition i == n
            i <= n,
        // the distance to n shrinks each round, so the loop ends
        decreases n - i,
    {
        i = i + 1;
    }
    i
}
}

Inference: for a hosted model that is not fine-tuned, the transferable part is the output contract (explain each annotation in terms of the obligation it discharges), not the training. Whether that contract alone raises Verus success is untested; the ablation below is for a fine-tuned 7B model.

Evidence. Table 4 (p.17), 105 theorems of Syscall_AI.thy, same 256-attempt setting:

• base model: 1/105 (0.95%)
• base model + CoT-based proof training: 24/105 (22.86%)
• base model + context augmentation: 6/105 (5.71%)
• both: 57/105 (54.29%)

Each percentage matches its fraction. Inference: the table has no row for fine-tuning on the same proofs without rationales, so it cannot separate the effect of the rationales from the effect of fine-tuning on seL4 proofs at all. The paper’s argument that rationales are what matters (§3.3, p.9) is not tested.

Where it fails. One pass means no feedback from the checker within an attempt; the method compensates with up to 256 independent attempts.

technique 3: targeted context in the prompt

What it is. Give the prover a short list of the definitions and lemmas the proof needs, instead of whole files. “Instead of supplying entire theory files, a compact set of definitions and lemmas that are necessary for understanding the theorem statement and completing the proof is supplied as proof context.” (§3.4, p.11)

When to use. In a large development where the transitive dependencies of a theorem do not fit, or drown the relevant facts.

How it is done (§3.4, pp.11-12).

1. The verifier supplies the context together with the theorem (p.11).
2. In the evaluation the context is read off the human proof (p.12, quoted above).
3. The paper’s example (Fig. 2 and p.11): for lec_ex_cap_to[wp] the context is the definition lookup_extra_caps_def and the lemma mapME_set; the generated proof unfolds the first and uses the second in (wp mapME_set | simp)+.
4. How to pick the context when no human proof exists: not in the paper.

Verus form. Inference: the context is the bodies of the spec fns that the function’s requires and ensures mention, plus the signatures (name, requires, ensures) of candidate lemma proof fns, and for vstd facts the names usable with broadcast use. A lemma’s body is not needed to call it. The step the paper leaves undone, choosing those lemmas, is the hard one in Verus as well.

Evidence. Table 4 above: context alone lifts the base model from 1 to 6 of 105; added to the fine-tuned model it lifts 24 to 57 of 105.

Where it fails. The reported rates are an upper bound for any pipeline that must find its own premises. The comparison to Selene’s 27.06% is not like for like, as the paper concedes in part: “Direct comparison with prior work on seL4 is difficult, as the only existing LLM-driven theorem proving efforts on seL4 adopt different theorem selection strategies and evaluation protocols.” (§4.2, p.14) §3.4 says Selene’s kind of setup supplied all transitively required theory files (p.11), so the two also differ in what context the prover received.

technique 4: whole-theory, checker-judged evaluation with an attempt budget

What it is. An evaluation recipe that avoids picking easy theorems and avoids counting fake proofs.

How it is done (§4.1, pp.12-14).

1. Fix the project version (seL4 as released on March 1, 2024; AFP of January 2026 with Isabelle2025-1).
2. Pick theories by a rule set by someone else: “Following the project guidance, for each proof category we select the first theory listed under Important Theories in the README and evaluate AutoReal-Prover on all theorems contained in that theory, without cherry-picking.” (§4.1, p.13) One exception is disclosed: for capDL-api the listed theories have no theorems, so KHeap_DP.thy, the one with most theorems, is used.
3. Replace each human proof by the generated one in place and run the checker.
4. Success needs three things: the proof “is accepted without errors, solves all subgoals, and contains no placeholder commands such as sorry or oops” (§3.1, p.7).
5. A theorem counts as proved “if at least one of up to 256 proof attempts is accepted by Isabelle” (§4.1, p.14).
6. Report the rate at smaller budgets too.

Verus form. Inference: take every function of a chosen module, strip the proof annotations but keep signature, requires, ensures and spec fns, let the system refill them, and run Verus. The counterpart of the placeholder rule is rejecting any output containing assume(...), admit() or a new #[verifier::external_body]. One extra check is needed that Isabelle gets for free: that the specification text is byte-identical to the original, because in Verus the specification sits in the same file the model rewrites.

Evidence, seL4, Table 2 (p.14), solved/total at 256 attempts:

• access-control Syscall_AC.thy 47/84 (55.95%)
• asmrefine SEL4GraphRefine.thy 1/1
• bisim Separation.thy 5/9 (55.56%)
• crefine Refine_C.thy 13/46 (28.26%)
• drefine Refine_D.thy 2/3 (66.67%)
• capDL-api KHeap_DP.thy 89/123 (72.36%)
• infoflow Noninterference.thy 101/233 (43.35%)
• invariant-abstract Syscall_AI.thy 57/105 (54.29%)
• refine Refine.thy 26/55 (47.27%)
• sep-capDL AbstractSeparation_SD.thy 0/1
• overall 341/660 (51.67%)

The columns add to 341 and 660 and each rate matches. Three theories have 1, 1 and 3 theorems, so “all 10 proof categories” rests on five theorems for three of them, and 356 of the 660 come from two theories.

By budget on seL4 (§4.2, pp.14-15): 37.12% at 5 attempts, 46.36% at 64, 50.00% at 128, 51.67% at 256. AFP overall (p.15): 36.36% at 5, 51.00% at 64, 52.55% at 128, 53.88% at 256.

AFP, Table 3 (p.15): CRYSTALS-Kyber_Security 32/64 (50.00%), RSAPSS 164/278 (printed 59.64%), Elliptic_Curves_Group_Law 47/109 (43.12%), overall 243/451 (53.88%).

Where it fails. Proofs come from existing theories whose statements, lemma structure and decomposition were made by experts. Nothing here measures stating a theorem, splitting it into lemmas, or proving against changed code. The paper reports no proof length for failed theorems and no time or cost per attempt.

technique 5: audit the rationales step by step

What it is. Check every generated explanation against the command it sits under.

How it is done (RQ3, §4.2, pp.15-16). Take all steps of all successful proofs (670 steps from 341 theorems), look for “reasoning errors or mismatches between the rationales and the corresponding proof commands”, and count by command type. Who did the looking, and how disagreements were settled: not in the paper.

Evidence. “Among these, 84 rationales associated with done contain irrelevant or incorrect explanations, often involving unrelated lemmas or theories.” (§4.2, p.15) Ten more are wrong elsewhere (for by simp, apply auto, apply wpsimp+). “Excluding done, the inaccuracy rate is 1.49%.” (§4.2, p.15)

Verus form. Inference: the audit can be partly mechanical in Verus. A comment claiming that an annotation discharges obligation X can be tested by deleting the annotation and checking that X, and only X, starts failing.

Where it fails. Rationales were audited only on proofs that passed. The case for their use in repair rests on one pair of proofs in Appendix B.2 (pp.24-27).

technique 6: check that passing proofs are not copies

What it is. Compare each accepted proof with the human one, to rule out recall of training text.

How it is done (RQ4, §4.2, p.16). Count proofs that differ from the original, and compare the number of “applied methods per proof, including Isabelle proof methods as well as referenced lemmas and definitions”.

Evidence. 93.55% of the 341 differ, which is 319, leaving 22 identical. Mean methods per proof: 6.018 generated against 6.123 original. Fig. 12 (p.28) shows one pair: the human proof uses clarsimp then wpsimp with thread_set_cte_wp_at_trivial; the generated one unfolds the definition, applies hoare_pre, then wpsimp with more general lemmas.

Verus form. Inference: carries over as a textual diff of proof annotations against the reference solution, useful whenever a benchmark’s reference proofs may be in a model’s training data.

Where it fails. “Differ” is not defined (exact string, or modulo whitespace and order). Inference: the base model’s 1/105 without context and 6/105 with it (Table 4) is stronger evidence against memorization than the diff.

inconsistent figures and missing information

• RSAPSS. Table 3 prints 164/278 as 59.64%; 164/278 is 58.99%. The overall 243/451 = 53.88% is consistent with 164, so the row’s percentage is the wrong figure. The text’s range “from 43.12% to 59.64%” (p.15) repeats it.
• rationale error rate. 10/670 = 1.49%, so the paper’s rate “excluding done” divides the non-done errors by all 670 steps. If the 670 include done steps, the denominator should be smaller and the rate higher; the paper does not give the number of done steps. With all errors counted the rate is (84 + 10)/670 = 14.0%.
• steps per proof. 670 steps over 341 proofs is 1.96 steps per proof, yet RQ4 reports about 6 methods per proof. Inference: the solved theorems are short proofs whose one or two commands each name several lemmas; the paper does not report the length of the human proofs of the 319 unsolved seL4 theorems, so how much harder those are is unknown.
• saturation. The paper says: “This indicates that performance saturates well before the maximum budget, with only marginal gains beyond 64 attempts.” (§4.2, p.15) From 64 to 256 attempts the seL4 rate goes from 46.36% to 51.67%, which is 35 more theorems of 660.
• Appendix B.2’s failed proof (Fig. 11, p.27). Its rationales say the attempt “is marked as failed” and that Isabelle “would not accept the proof”, and they compare the attempt with a better strategy. The model writes rationales before any check, so text that knows the verdict is not what a failed attempt would normally contain. Inference: the failed-case rationales shown were not produced the way inference-time rationales are, and the case study does not show that rationales reveal failure.
• hold-out. Only the evaluation theorems’ own steps are excluded. The paper does not say whether FVELER’s traces come from the same seL4 version as the March 2024 evaluation copy, or whether lemmas near-identical to test theorems remain in training. For AFP there is no fine-tuning data, but the base model’s pretraining exposure is not discussed.
• abstract against body. The abstract counts as a contribution that the model “enables step-wise explanations alongside proofs”; 84 done explanations are wrong, so at most 84 of the 341 successful proofs (up to about one in four) carry a wrong closing rationale; the paper does not say how many proofs end in done.

not to redo in VL

Inference:

• measuring a prover with oracle premises is done here and gives about half of real seL4 theorems for a 7B model; repeating that for Verus would only show the same upper bound. The open measurement is with premises selected automatically
• the evaluation recipe of technique 4 (theories chosen by an outside rule, every theorem, checker verdict, placeholder ban, several budgets) is sound and can be reused as is
• building step rationales with an unchecked small model is cheap and was done; what was not done is checking them, or showing they beat plain fine-tuning

threat to VL’s product

Inference: low. This is proof filling for existing Isabelle theorems with hand-picked premises; it does not write specifications, code, or new lemma structure, and it does not target Rust. The part to watch is cost: if a locally run 7B model reaches half of seL4’s theorems under an oracle, the proof-filling step of a Verus pipeline may also be doable by a small fine-tuned model, and a product whose only edge is proof filling with a large hosted model would have little margin. The paper’s own limit applies to that reading: it gives no cost, time, or hardware figures.

techniques for the catalog

• step-level rationale data: pair each proof step with the state before and after and have a model explain the change, to build training data from an existing proof corpus
• held-out construction: remove every step of the evaluation theorems before generating any training rationale
• interleaved proof and rationale output: train or prompt the model to emit each proof command followed by a comment on its effect, producing the whole proof in one pass
• targeted proof context: supply only the definitions and lemma statements the proof needs, not whole files
• oracle-context evaluation: take the context from the human proof to isolate proof writing from premise selection, and report it as such
• whole-theory evaluation by outside rule: evaluate every theorem of theories named by the project’s own documentation
• placeholder ban in the success criterion: a proof counts only if the checker accepts it with all goals closed and no sorry or oops
• attempt-budget curve: report success at 5, 64, 128 and 256 independent attempts
• step-level rationale audit: count wrong explanations per command type across all passing proofs
• copy check against reference proofs: report the share of accepted proofs that differ from the human proof and compare method counts
• two-factor ablation on one theory: base, training only, context only, both, on a fixed 105-theorem set

Last edited: 2026-10-13