Lemur: Integrating Large Language Models in Automated Program Verification

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

scope and prior notes

The batch describes this ICLR 2024 paper by Haoze Wu, Clark Barrett, and Nina Narodytska. I found no earlier paper-specific walkthrough in the research notes (the shortlist mentions it only). This study reconstructs the paper’s complete verification workflow from the main text and appendices so a Verus engineer can implement the transferable parts without opening the paper.

The paper’s central claim is a sound interface between an LLM that suggests predicates and a conventional verifier that checks them. The authors state: “We formally describe this methodology as a set of transition rules and prove its soundness.” (abstract, p. 1). The LLM never gets to certify its own suggestion: “properties generated by an LLM are treated as assumptions until we can prove that they are invariants of the original program” (Sec. 3, p. 3). That separation is the main reusable technique.

technique 1: model verification as assumptions, implications, and a trail

What it is. Represent a reachability property as p = <predicate, program line>. An assumption q modifies execution so a path stops when q is false. Define q ->_P p to mean p is invariant in the program with q assumed. A verifier V(P,A,p) returns TRUE, FALSE, or UNKNOWN for whether assumptions A imply p. The proof state is <P,A,M>, where M is a trail of proof goals and A is empty or one proposed assumption. This turns a single hard invariant into a chain of smaller implications.

When to use it. Use this decomposition when a backend can prove simple invariants but returns UNKNOWN on the target. It is useful for loop invariants, range facts, and arithmetic relations that are easier to prove at an earlier program point. The paper’s running example proves x != 30 for a loop adding four to x by first finding x % 4 == 0.

How to do it.

1. Encode the target p at its assertion location and call V(P, empty, p)
2. If V is UNKNOWN, ask an oracle for candidate q at an earlier location
3. Check V(P,{q},p), which tests implication under the assumption
4. If implication is TRUE, append q to M and recursively prove q with no assumption
5. If q is proved, compose q -> p with q’s invariant proof
6. If q is stable but not proved, separately prove p under not q and use the two cases

The paper’s formal configuration is explicit: “The calculus operates over a configuration, which is either one of the distinguished symbols {SUCCESS, FAIL} or a tuple <P, A, M>” (Sec. 3, p. 3). Its example says the proposed x % 4 == 0 is inductive and lets k-induction finish (Example 3.1, p. 5).

Verus form (inference). Make q a requires-like ghost predicate or a lemma precondition, and make p an ensures/invariant assertion. Use assert(q ==> p) or a lemma proving implication, then a separate lemma proving q for all loop iterations. Verus’s invariant clause is the natural place for q; assume must not be used as a final certificate because it is trusted. The trail is a ghost list of pending predicates if implementing a search driver outside Verus. The stability split corresponds to proving both q and !q cases with assert forall|...| or two lemmas. The paper is about C verifiers, so this mapping is an inference; its implication relation and proof composition carry over, while C line locations and an executable assumption that terminates paths do not.

Evidence and limits. Soundness is a theorem conditional on V: “Given a property p0 and a program P, if SUCCESS is reached by a sequence of valid rule applications starting from <P, empty, [p0]>, then p is an invariant on P.” (Theorem 3.1, Sec. 3, p. 5). The trusted base therefore includes V’s soundness and the semantics of assumptions; LLM output is not trusted. The method can return UNKNOWN and does not make an incomplete backend complete.

technique 2: the LEMUR transition rules for propose, decide, repair, backtrack, and split

What it is. The calculus supplies seven transitions. Propose replaces an empty assumption with q when V cannot decide p. Decide turns q into a new goal when V proves q implies p. Repair 1 replaces q when implication is UNKNOWN; Repair 2 replaces q after proving q false. Backtrack returns to the prior goal and tries another q. Success 1 accepts a directly proved goal. Success 2 accepts a stable q when both q -> p and not q -> p hold. Fail accepts a counterexample only for the original goal.

When to use it. Use Repair 1 for a weak candidate, Repair 2 for a false candidate, and Backtrack when a branch is unproductive. Use Success 2 for disjunctive or case-based facts where proving q itself is unnecessary. Keep the original program unchanged; only the proof state evolves. The authors emphasize this design: “the program P remains unchanged in every rule” (Sec. 3, p. 4).

How to do it step by step.

1. Initialize <P, {}, [p0]>
2. Call V on the last trail item with the current assumption
3. Return FAIL immediately only when V says the original p0 is false
4. On UNKNOWN, call Opropose(P,p) and try one q
5. On TRUE for V(P,{q},p), recurse on q (Decide)
6. On UNKNOWN, call Orepair(P,p,q,UNKNOWN) (Repair 1)
7. On FALSE while q is a pending goal, call Orepair(P,p,q,FALSE) (Repair 2)
8. If a pending goal fails and alternatives remain, pop to the previous p and try another proposal (Backtrack)
9. For a stable q, prove p under !q; if TRUE, use Success 2

The paper’s exact rule-level description says: “The Repair 1 rule can be applied when the current assumption q is not sufficient for the verifier to prove the current proof goal p.” (Sec. 3, p. 4). For the case split, it says: “the current proof goal q :=” is stable and “the verifier is also able to also prove p under the assumption” (Sec. 3, p. 4).

Verus form (inference). Implement each transition as a Rust host-side search over generated Verus snippets, while Verus checks each candidate lemma. Repair means ask the model for a stronger invariant or lemma statement after feeding the verifier result. Backtrack is ordinary search over a queue. Success 2 is two Verus proof branches guarded by if q { ... } else { ... }, with both branches proving the target. Do not encode an unproved q as assume; instead, compile and verify every branch. The exact V result vocabulary (TRUE/FALSE/UNKNOWN) is a paper abstraction, not a Verus API.

Evidence and limits. The soundness proof composes implication transitivity and the stable split (Lemma 2.1, Appendix B; Theorems 3.1–3.2). Failure is meaningful only when V is sound; UNKNOWN is inconclusive. Rule selection is a heuristic when several rules apply, so search order affects runtime but not the theorem.

technique 3: bounded, terminating recursive algorithm

What it is. Algorithm 1 (lemur_check) turns the calculus into a terminating procedure. It limits each goal to k proposals and requires every generated predicate q at a strictly smaller program line than p: “must contain a smaller program line number than the one in the current proof goal” (Sec. 4, p. 6). The decreasing line number bounds recursion depth; k bounds branching.

How to do it.

1. Call d = V(P,{},p); return FAIL or SUCCESS for FALSE or TRUE
2. Otherwise set Q = Opropose(P,p) and i=0
3. While i < k and Q is nonempty, pop q and test e=V(P,{q},p)
4. Return FAIL if e is FALSE
5. If e is TRUE, recurse on q
6. Return SUCCESS if recursion succeeds; otherwise apply stable split or repair
7. Add repaired candidates to Q for UNKNOWN or false recursive results
8. Return UNKNOWN after k attempts

The pseudocode’s contract is explicit: “Output: SUCCESS only if Inv(P, p); FAIL only if ¬Inv(P, p); and U NKNOWN if inconclusive.” (Algorithm 1, p. 6). Termination is proved because every recursive q has a smaller line number and the loop is finite (Theorem 4.1, Sec. 4, p. 6).

Verus form (inference). Use a bounded work queue of candidate invariant lemmas and a recursion-depth measure tied to syntactic block order, loop nesting, or source span. Verus can prove each generated candidate but is not itself the orchestration loop; a Rust driver can invoke verus repeatedly. A decreasing source-line measure is less natural in Rust, so use a well-founded ghost rank (for example, number of unresolved loops before the target) and require generated subgoals to reduce that rank. Preserve the UNKNOWN outcome when the bound expires.

Evidence and limits. The calculus is sound even without these bounds, but the unbounded calculus may not terminate. Bounds trade completeness for a predictable result; the paper reports no guarantee that a successful candidate will be found within k. A too-small k or overly strict location condition yields UNKNOWN rather than an unsound proof.

technique 4: prompt engineering as a verifier-facing parser

What it is. The oracle is constrained to emit machine-extractable assertions. The authors found chain-of-thought output verbose and unreliable, so they force a format: “Your output should be ‘assert(…);// Line number’” (Sec. 5.1, p. 7). They insert marker lines (// Line A) at loop boundaries because models miscount lines, then parse and deduplicate assertions by abstract-syntax-tree equivalence. They call the model multiple times and rank proposals by frequency, breaking ties with shorter expressions.

How to apply it.

1. Insert named markers immediately before and at loops
2. Include the complete program, target assertion, marker names, and whether to produce facts or loop invariants
3. Instruct: “Don’t explain” and require assert(...); // line A
4. Sample several prompts/penalties
5. Parse only syntactically valid assertions
6. Normalize equivalent ASTs and rank by proposal frequency, then expression length
7. Send candidates to V; never trust text that does not compile

Appendix F gives the exact template: “Print [P2] as valid C assertions at line[P3] [P4] that help prove the assertion. Use ‘&&’ or ‘||’ if necessary. Don’t explain.” (Appendix F.1, p. 17). Its worked output generated assert(i <= n); and assert(s >= 0 && s <= i*UCHAR_MAX); for a loop summing random unsigned chars (Appendix F.1, pp. 17–18).

Verus form (inference). Replace C assert with a restricted Verus syntax such as invariant clauses, requires, ensures, or standalone lemma signatures. Use stable symbolic labels for loop heads and function boundaries instead of line numbers. Parse with a Rust/Verus AST or a narrow grammar, then compile before verification. AST canonicalization and frequency ranking transfer directly; C integer-width idioms such as UCHAR_MAX need Rust type-aware translation.

Evidence and limits. Formatting reduces extraction errors but does not establish semantic correctness; V remains the checker. The authors report that line markers mitigate off-by-one locations and that GPT-4 can propose modulo facts absent from the program, but proposal quality is stochastic and depends strongly on model and prompt.

technique 5: use established backend proof engines as the low-level checker

What it is. LEMUR delegates concrete reasoning to sound automated verifiers. The paper discusses bounded model checking (BMC), k-induction, and predicate abstraction. BMC unrolls to bound m and finds finite counterexamples; k-induction checks k-step initiation and an inductive step; abstraction proves properties on an over-approximation and refines when a spurious counterexample appears. Their prototype uses ESBMC (k-induction) and UAutomizer (predicate abstraction), with a 30-second timeout per call.

When to use it. Use BMC for shallow bug finding, k-induction for loop invariants, and abstraction when a compact predicate domain can summarize states. LEMUR’s LLM supplies the missing high-level predicate; the backend supplies the proof obligation and counterexample/UNKNOWN signal.

Verus form (inference). Verus’s SMT-backed verification condition generator is the backend V. Loop invariants and decreases clauses correspond to the facts k-induction needs; quantified lemmas and triggers provide the abstraction predicates. A timeout or failed verification should map to UNKNOWN, never to FALSE. BMC itself is not a Verus feature, so this is an architectural analogy.

Evidence and limits. The paper explicitly notes incompleteness: “k-induction is not complete; there are properties that are not k-inductive for any k” (Appendix A, p. 13). Modern verifiers handle relatively small programs, and even a strong invariant may not solve a task. Backend soundness and timeout policy are trusted assumptions.

measured results and what they establish

On 133 Code2Inv benchmarks, ESBMC alone solved 68, LEMUR GPT-3 solved 103, and LEMUR GPT-4 solved 107 within a ten-minute limit; average solved-instance times were 0.34 s, 35.6 s, and 32.9 s, with 0, 8.6, and 4.7 proposals respectively (Table 1a, p. 8). On 47 SV-COMP benchmarks that ESBMC and UAutomizer could not solve within ten minutes, the baselines solved 1 each, LEMUR GPT-3 solved 14, and GPT-4 solved 25 under a 15-minute per-instance limit; GPT-4 averaged 7.2 proposals and 234.5 s for solved instances (Table 1b, p. 8). The text says: “LEMUR (GPT4) is able to solve 25 of the 47 SV-COMP benchmarks” (Sec. 5.3, p. 8).

These denominators and timeouts support improved benchmark coverage, not general correctness beyond the backend’s trusted semantics. Three repeated runs show stochastic variance: GPT-4 with repair solved 25, 24, and 24; without repair 19, 20, and 20 (Table 3, Appendix G, p. 19). The paper also reports 8 solved SV-COMP cases with two loops and 5 with three or more, but does not provide per-program proof sizes or a failure taxonomy. The 47 in the Table 1b caption is the size of the SV-COMP benchmark set, not a solved count; the inconsistency is that Section 4.2 (p. 9) says LEMUR (GPT4) solved 25 of the 47 yet later says “12 of the 26 solved instances” for Figure 4, while Table 1b and the headline run report 25 (the best of three runs in Table 3 is also 25), and the paper does not say which is right. This is an internal counting inconsistency worth preserving rather than silently correcting.

trusted, missing, and already-done work

Proved by the paper: the transition rules preserve invariant truth; SUCCESS and FAIL are sound assuming V; the bounded algorithm terminates; the prototype improves these benchmark counts. Measured but not proved: LLM semantic understanding, proposal usefulness on unseen languages, scalability to real C libraries, and transfer to Rust/Verus. Trusted: V’s soundness, C/SMT semantics, parser correctness, timeout interpretation, and the OpenAI API responses as suggestions only. Not trusted: any unverified LLM predicate or code rewrite.

VL should not redo the already-demonstrated pattern of letting an LLM directly edit verified code or treating generated invariants as facts. The paper explicitly contrasts this with ESBMC-AI, which assumes LLM rewriting is syntactically and semantically correct (Sec. E, p. 16). VL’s remaining work is a Verus-native candidate grammar, source-label mapping, AST deduplication, bounded search, and empirical evaluation on Rust loops. Threat to an agent-written verified-Rust product (inference): medium. The architecture can increase proof throughput while preserving Verus as checker, but a parser or orchestration bug could omit obligations, and LLMs may propose unsound-looking specifications that are accepted only if the driver accidentally uses assume or weakens a postcondition. Treat generated predicates as untrusted input and audit the generated Verus command and specification diffs.

techniques for the catalog

• assumption-trail decomposition — represent a hard invariant as verifier-checked implications through a trail of smaller predicates
• sound propose/decide/repair/backtrack calculus — search with explicit transitions while proving LLM suggestions before accepting them
• stable case split — prove both q and not q implications when q is stable, even if q itself is not invariant
• bounded terminating search — cap proposals and require a decreasing subgoal rank to return SUCCESS, FAIL, or UNKNOWN
• verifier-facing prompt grammar — use named program markers, strict assertion output, repeated sampling, and AST deduplication
• backend cooperation — combine LLM high-level predicates with BMC, k-induction, abstraction, or Verus SMT checking

study status

Read the complete extracted text, including appendices, after confirming the first-page title. Quotes were selected from the PDF text and include section/page pointers. The study is staged for the paper gate; it has not been copied into the human notes.

Audited 2026-10-12 against the paper: read the full text including appendices A-G; checked the calculus rules (Fig. 1), Algorithm 1 steps, Condition 1, Theorems 3.1/3.2/4.1, Table 1a/1b figures, the 25/24/24 and 19/20/20 rerun counts in Table 3, the 12-of-26 versus 25 inconsistency, prompt template and F.1 example, the ESBMC-AI contrast, and the Verus-form paragraphs (marked inference, sound as analogies). Changed one page reference: the k-induction incompleteness sentence is on p. 13 (Appendix A), not p. 12. No other defects found.; follow-up: the lemur 47 versus 26 versus 25 item confirmed in part, the caption’s 47 is the benchmark-set size and the real conflict is 26 solved in prose against 25 in the table, sentence corrected.

Last edited: 2026-10-13