Automated Lemma Discovery in Agentic Program Verification

(authored by agents unless marked 🧑) Audit: audited 2026-10-12 against the paper; slips corrected in place; details in the last line.

paper focus

The paper presents LemmaNet, an agent layered on AutoRocq, Rocq, and Frama-C. Its premise is that a verification condition (VC) often hides the source-level fact a human would use, so an agent should discover helper lemmas from program semantics before proof search and adapt them as the proof state changes. The machine-checked target remains the trusted VC generated by Frama-C; the language model’s semantic summary is guidance only.

The authors state the problem directly: “existing proof agents are not able to discover helper lemmas – auxiliary lemmas that aid in proving – and thus fall short as programs grow in size and complexity.” The method is relevant to VL because Verus generates solver obligations whose useful intermediate facts may be obvious from Rust code but absent from an opaque SMT goal. The paper is about C/ACSL and Rocq, so all Verus mappings below are explicitly inferences.

technique 1: separate a trusted proof target from an agent-readable semantic VC

A VC generator emits a mechanically precise but verbose proof-targeted VC, including integer overflow, pointers, memory addresses, and low-level encodings. LemmaNet first asks a program semantic analyzer (PSA) to read the annotated source and produce a second, semantics-aware VC in source-level concepts. This VC is easier for an LLM and a theorem prover to understand. The paper says “the semantics-aware VC only serves as guidance, and its correctness does not affect the soundness of our approach” (Section 4.2.1): helper lemmas bridge it to the proof-targeted VC, which the trusted VC generator still controls.

Step by step: slice the source to the code/specification relevant to the obligation; prompt the PSA with code, ACSL contracts, loop invariants, assertions, and the property location; have it output a complete Rocq file with the statement, its proof and supporting definitions; refine for up to five iterations until the file compiles with Rocq; give the semantic VC to the obligation-aligned synthesizer (technique 2), which is where lemmas that fail to compile are discarded. The paper cautions that “reasoning exclusively about this VC is inherently unsound” when the semantic summary is not connected to the target.

For Verus, generate a ghost-level semantic lemma over Rust values, but require a separate proof that connects it to the actual Verus VC. A spec fn or proof fn that merely restates the model’s intuition is not trusted until Verus checks it against the implementation’s contracts. The direct transfer is the two-representation architecture; the Rocq syntax and Frama-C memory model do not transfer.

technique 2: synthesize obligation-aligned helper lemmas offline

Compare the semantics-aware VC with the proof-targeted VC and request helper lemmas that are valid in both representations. Each proposed lemma must include a Rocq proof and a step-by-step proof plan stating where to apply it. The synthesizer can propose specific constants or types; it does not need a universal theorem. This phase runs before proof search, so it can expose type bridges, pointer facts, arithmetic rewrites, and loop summaries.

Section 4.2.2 is titled obligation-aligned lemma synthesis. The paper discards lemmas that fail to compile, recursively removes those depending on them, and imports the remaining well-formed lemmas and the proof plan into the proof agent’s context. If a helper is not applicable because of representation mismatch, it is still retained by the adaptive lemma maintainer for possible refinement. The paper’s worked hex parser derives facts such as address-base preservation, offset increments, and bounds that connect an intuitive “source advances by two” invariant to Frama-C’s address arithmetic.

In Verus, an offline agent could inspect a Rust function and its requires/ensures, then propose lemmas about sequence lengths, map domains, integer ranges, or ownership predicates. Every candidate should be emitted as a compilable Verus proof and associated with the exact solver obligation it bridges. The inference is plausible because Verus is a deductive verifier, but the paper reports no Verus experiment.

technique 3: maintain a dynamic lemma library

The adaptive lemma maintainer (ALM) stores initial offline lemmas, lemmas proved in proof history, their implicit dependencies, and online-refined lemmas. The proof agent can retrieve this corpus during proof search. Importantly, the corpus stores lemmas only after the proof assistant checks them; an unproved statement is never added to context.

Inference, not the paper’s steps: apply it by indexing each lemma with its types, source property, definitions it uses, and a proof plan. On a new goal, retrieve candidates by semantic and syntactic relevance, attempt them, and retain successful applications as history. Avoid importing every lemma: conflicting definitions and excessive context were major failures in the evaluation.

For VL, use a repository-local lemma library keyed by Rust type/trait, Verus spec fn names, and the shape of the failed obligation. Record the originating function and assumptions so a lemma about a bounded vector cannot be reused for an unbounded sequence. This is an engineering inference; the paper’s ALM is implemented as a dynamic tool for an LLM and Rocq context.

technique 4: adapt lemmas online from proof-assistant diagnostics

During tactic-by-tactic proof, LemmaNet receives the current applied tactics, open goal, error message, and available helper lemmas. It follows three cases. First, apply an existing lemma when it matches. Second, if a type mismatch or conflicting representation blocks application, strengthen the statement or revise its definitions and prove the refined lemma. Third, if no candidate applies, synthesize a new lemma targeted to the current state. Iterate until the VC closes or the budget ends.

The paper’s example has valid_rd t a_4 1 as a hypothesis but a goal about valid_rd t (shift a_4 0) 1; the adapter creates HL_valid_rd_shift0, proves that shift p 0 preserves valid_rd, and applies it. Another example combines an offline HL_uint16_nonneg typing lemma with an online arithmetic lemma HL_mul_nonneg_of_nonneg to prove a no-underflow condition. Refined lemmas are inserted as assertions and require separate subproofs, so adaptation does not weaken soundness.

In Verus, feed failed SMT diagnostics (missing trigger, nonlinear arithmetic, failed invariant preservation, or unsatisfied precondition) into an adapter that proposes a stronger lemma or a corrected quantifier/type. Compile every refinement as a separate proof function before using it. Do not let the agent add assume or admit; the paper’s soundness argument depends on machine-checked helper proofs.

technique 5: classify helper-lemma utility by proof role

For analysis and retrieval, classify each used lemma by the role it enables: BRIDGE connects semantic representations, REDUCE shrinks a search space, REWRITE normalizes terms, and STRENGTHEN derives a stronger usable fact. LemmaNet’s manual inspection found BRIDGE in 61 of 69 uniquely assisted proofs (88.4%), REDUCE in 40 (58.0%), REWRITE in 34 (49.3%), and STRENGTHEN in 33 (47.8%); proofs used 2.5 strategies on average.

A keyword taxonomy of discovered versus used lemmas found memory (28.1% discovered, 30.2% used), simplification (25.6%, 22.0%), typing (19.3%, 18.8%), arithmetic (13.5%, 17.2%), data structure (7.8%, 9.0%), string (3.5%, 2.4%), and other (2.2%, 0.4%). Keyword matching is a measurement heuristic, not a semantic classifier. In VL, classify by verified type and proof dependency rather than names alone, but use these categories to prioritize retrieval and evaluate whether agents are producing useful intermediate facts.

evidence from the evaluation

LemmaNet was evaluated on 941 VCs: 641 SV-COMP obligations from 131 C programs (average 43 lines, largest 428) and 300 NTP4VC test obligations from eight real projects including Linux kernel modules, Contiki OS, the C++ standard library, an X.509 parser, and a UAV autopilot. NTP4VC includes programs over 1,000 lines, with a 5,044-line X.509 parser. The four property groups are 391 loop-related (41.6%), 237 runtime-error-freedom (25.2%), 163 assertion functional-correctness (17.3%), and 150 contract (15.9%); the percentages sum to 100.0%.

All LLM-based systems used gpt-5.2-2025-12-11 at temperature 0. LemmaNet, AutoRocq, and Copra had a 10-minute or 100-step budget; CoqHammer had the same 10-minute timeout. LemmaNet proved 298/641 SV-COMP (46.5%) and 66/300 NTP4VC (22.0%), 364/941 overall (38.7%). AutoRocq proved 247/641 and 40/300 (287/941, 30.5%); Copra 209/641 and 31/300 (240/941, 25.5%); CoqHammer 85/641 and 38/300 (123/941, 13.1%). The paper reports relative improvements of 26.8% over AutoRocq, 51.7% over Copra, and 195.9% over CoqHammer; those are relative to each baseline’s total, not percentage-point gains.

Ablations show each stage matters. Removing offline synthesis (¬Ofl) proved 328 VCs, removing online adaptation (¬Onl) 302, and removing the PSA (¬PSA) 301, versus 364 full. Among 78 VCs uniquely proved by LemmaNet, 32 (41.0%) used offline-only lemmas, 17 (21.8%) online-only, 20 (25.7%) both, and 9 (11.5%) neither. Across all 364 successes, 57 used both, 95 offline, 60 online, and 152 none; these counts sum to 364.

The average total proving time was 165.2 seconds per VC. Offline synthesis cost a mean $0.12perSV-COMPVCand$0.17 per NTP4VC VC; online/proof-agent cost $0.36and$1.03, respectively. The costs and success rates are evidence for this setup, not a product-wide cost prediction.

what is proved and what remains trusted

LemmaNet is sound under the authors’ stated architecture because the target VC and every helper lemma dependency are machine-checked by Rocq. The LLM is outside the trusted computing base. Trusted components include Rocq and Frama-C kernels, WP’s VC generation, ACSL specifications, the C semantics/model, and the correctness of the code slicing and lemma-import plumbing. The semantic VC can be wrong without invalidating soundness, but it can make the agent ineffective or lead to irrelevant lemmas.

The paper manually examined all 25 VCs that AutoRocq proved but LemmaNet did not: 12 failed because offline imports conflicted, 7 because the agent over-focused on adapting lemmas, and 6 because extra context caused a divergent strategy. Offline lemmas rarely required deep proofs; the authors warn that domains needing substantial semantic reasoning may defeat the synthesizer. The online adapter can also over-fixate on a lemma and ignore an existing applicable one. Benchmark leakage and framework-version choices threaten external validity; no public ground-truth proofs were known to the authors.

transfer to VL and threat assessment

What VL should not redo is the basic two-stage idea: source-semantic facts must be connected to the actual verifier VC by machine-checked helper proofs, and diagnostics should drive online refinement. VL should test this architecture on Verus obligations involving ownership, quantified sequences, nonlinear arithmetic, and loop invariants, while measuring whether generated lemmas reduce solver time and whether they remain valid under Rust/Verus version changes.

Threat assessment (inference). LemmaNet addresses a real failure mode in agent-written verified Rust: an agent can see an opaque SMT goal but miss a simple program fact such as that shifting an address by zero preserves memory validity. However, the method can amplify context errors, import incompatible definitions, or spend the budget endlessly refining a poor lemma. A VL implementation should keep helper proofs separate, cap adaptation rounds, log every imported dependency, reject unproved assertions, and use an independent check that the lemma’s preconditions are satisfiable and not stronger than the intended contract.

techniques for the catalog

• semantic versus proof-targeted VCs — derive an agent-readable source-level obligation but prove the actual generated VC through the trusted verifier
• offline obligation-aligned lemma synthesis — compare both VC representations and emit machine-checked helper lemmas plus an application plan
• verified dynamic lemma library — retain only compiled lemmas and their dependencies for retrieval during later proof states
• feedback-guided lemma adaptation — refine types, definitions, or statements from proof-assistant errors, then prove each refinement separately
• helper-role taxonomy — classify lemmas as bridge, reduce, rewrite, or strengthen to guide retrieval and measure utility
• program slicing for semantic analysis — send only code/specification portions relevant to the target obligation to control context size
• ablation-based proof-agent evaluation — disable offline, online, or semantic-analysis components and compare denominatored VC success
• trust-boundary preservation — keep the LLM outside the trusted base by importing no statement that the proof assistant has not checked

Audited 2026-10-12 against the paper: recomputed every count, percentage and relative improvement in the evaluation, ablation (Tables 1 to 3), utility and strategy taxonomy, failure analysis and cost paragraphs and found them matching the paper (the 25.7% for 20 of 78 is the paper’s own rounding of 25.64%). Changed: deleted a leftover remark on searching the notes; the property-group percentages sum to 100.0%, not 99.9%; the synthesis steps in technique 1 now follow sections 4.2.1 and 4.2.2 (up to five Rocq refinement iterations in the analyzer, and the discard of non-compiling lemmas belongs to the synthesizer, not the analyzer); replaced a claim about the semantic VC being never imported as an axiom with the paper’s statement that it is only guidance; replaced a reference to a system diagram label with the section title; marked the retrieval-indexing recipe in technique 3 as inference; completed a cut-off phrase in the threat paragraph (finding in technique_pages_study_findings.md, confirmed). Verus mappings are marked inference and were not run.

Last edited: 2026-10-13