A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number in Tables 1 and 2 (including each average and reduction recomputed from its fractions), page and section references, quotations, the steps of techniques 2 to 6 against Section 5 and Algorithm 1, and the Verus forms; corrected the ablation paragraph (per-benchmark claim for feedback alone and a comparison the ablation cannot make), the baselines 15-hour claim widened from typically to on any of the four, the Verus loop paragraph (loop isolation), and four unmarked inferences or widened summary lines.

source: Wang, Lin, Chen, Li, Yang, Yi, Qin, Luo, Li, Gu, Lu, Yin, arXiv:2512.24594v2 (10 Mar 2026); Proc. ACM Program. Lang. 10, OOPSLA1, Article 160, 31 pages with appendices A-D. A page given as p.N is article page 160:N.

terms used below, as the paper defines them

• RTE: runtime error, such as division by zero, overflow, invalid memory access, read of uninitialized memory
• RTE assertion: an assertion a static analyzer inserts in front of an instruction that may cause an RTE; it states what must hold for the instruction to be safe
• guard assertion: an RTE assertion, or a check of a callee’s precondition at one call site
• hypothesis: a guard assertion the tool could not prove and hands to a human

the claim, the proof, and what rests on trust

Preguss is a tool for C that makes an LLM write ACSL contracts and loop annotations until the deductive verifier Frama-C/Wp proves that analyzer-reported possible runtime errors cannot happen. The abstract’s one-sentence description: “Preguss synergizes between static analysis and deductive verification by steering two components in a divide-and-conquer fashion: (i) potential runtime error-guided construction and prioritization of verification units, and (ii) LLM-aided synthesis of interprocedural specifications at the unit level.” (Abstract, p.1).

proved on paper: Theorem 20 (soundness, p.15, proof in Appendix A.2, pp.29-30): what the tool returns as verified is valid given the returned hypotheses. Theorem 21 (termination, p.16), as a proof sketch.

measured: programs fully verified on a 51-program suite; on four real modules of 544 to 1,451 lines, the share of guard assertions proved and the number of specifications a human had to add, fix or remove afterwards.

trusted:

• the static analyzer is assumed to report every possible RTE; the paper names the limit: “Regarding the former, abstract interpretation-based static analyzers like Frama-C/Rte and Frama-C/Eva typically target specific categories of UBs and RTEs, which may limit the soundness of Preguss in guaranteeing RTEfreeness for those categories.” (Section 6.7, p.24)
• Frama-C/Wp and its SMT solvers are assumed sound (Definition 9, p.5)
• every hypothesis left over is unproved until a human checks it (Theorem 11, p.9)
• contracts for library functions without source, such as memcpy and memset, are written by hand (Section 6.3, pp.20-21)
• for SAMCODE, floating-point alarms are left out (Table 2 note, p.20) and a hand-built generalization of the entry point is used (Section 6.1, p.17)
• no functional correctness is claimed; the target is absence of runtime errors only

technique 1: let the analyzer’s alarms be the verification goals

what it is: run a sound abstract-interpretation analyzer first and treat each alarm it inserts as the property the LLM must make provable, instead of asking the LLM to describe what the function does. The paper’s statement: “One can leverage RTE assertions from abstract interpretation-based analyzers – as targets for RTE-freeness verification – to guide LLMs to synthesize specifications effectively.” (Insight 1, p.6).

Inference: use it when the goal is a safety property that a tool can enumerate as program points (the paper says other annotated properties can replace RTE assertions, Section 5.4, p.16).

the paper’s example (Fig. 1, p.5): for abs(int x) the analyzer inserts assert INT_MIN < x before return -x. Given that assertion, an LLM writes the precondition requires INT_MIN < x; checking it at the two call sites separates abs(-42) (safe) from abs(INT_MIN) (a real error). Given only the source, an LLM tends to write the postcondition describing the result, which the verifier cannot prove for INT_MIN and which does not locate the bad call.

evidence: the baseline AutoSpec with RTE assertions added (AutoSpecRte) verifies 22 of 51 programs in at least one of three trials, AutoSpec alone 17 of 51 (Table 1, p.18). The paper states this as a 29.4% increase (5/17, a relative figure). Average success rates over three trials: 41.8% against 32.7%.

limits: alarms alone are not enough; the paper reports the remaining gap to the full tool (technique 5 and 6 results) as evidence that the simple extension is insufficient (Section 3.1, p.6).

Verus form. Inference: Verus needs no separate analyzer for this class. Run on code with no annotations, Verus itself reports each possible arithmetic overflow, out-of-range index, division by zero and unmet callee precondition as a failed obligation with a location. That list plays the role of the RTE assertions. The agent is then asked to make each reported obligation provable, not to write a full ensures. What does not carry over: uninitialized reads and invalid pointers are excluded by safe Rust’s type system, so the alarm list is shorter and mostly arithmetic and indexing.

technique 2: verification units, one guard assertion plus a two-layer slice

what it is: split the whole task into one unit per guard assertion. Definition 15 (p.12): a V-Unit is a guard assertion together with a program slice holding the assertion’s host function and that function’s direct callees.

why this slice is enough: “Consequently, to validate an individual RTE assertion 𝛼, it suffices to extract a minimally constrained program context consisting of the host function of 𝛼 and all its callees.” (Section 5.1.2, p.12). The reason given is modular verification: proving a function needs its own body and its callees’ contracts, nothing else.

how it is done (Section 5.1, pp.10-12):

1. run the analyzer to insert RTE assertions (step ❶ of Fig. 4)
2. build the call graph and record every call site (step ❷)
3. create a guard assertion for each call site as a precondition check whose predicate is not yet known: “Thus, we statically extract all precondition check locations through call-graph analysis (❷) without generating actual specifications, initializing each predicate to the tautological true as a placeholder.” (Section 5.1.1, p.10)
4. make one V-Unit per guard assertion (RTE assertions and call-site checks alike)
5. order the units into a queue (technique 3)

the paper’s example (Fig. 5, p.11): id.c has one RTE assertion (division by zero in one) and four call sites, hence five V-Units.

Verus form. Inference: a unit is one failing Verus obligation plus the text of its function and the signatures with requires/ensures of the functions it calls (their bodies are needed only in the callee stage of technique 5). Call-site precondition checks exist in Verus without any bookkeeping: once a callee has a requires, Verus checks it at each call.

limits named by the paper (Section 7, p.24): a host with many callees may still exceed the context window; global and external variables are left out of the slice, which can cause false alarms.

technique 3: bottom-up queue with a source-order tie-break

what it is: a total order on V-Units (Definition 16, p.12). Unit i comes before unit j if j’s function is an ancestor of i’s function in the call graph; if neither function is an ancestor of the other, the unit whose instruction has the smaller line number comes first.

why: callee contracts must exist before callers are verified; inside one function an earlier assertion is often a hypothesis for a later one, so proving it first may produce the specifications the later one needs (Section 5.1.2, p.12). All properties inside a loop are treated as mutually dependent and get equal priority.

restriction: “Preguss admits, in its current implementation, merely acyclic call graphs.” (Remark, p.11). The stated cause is Frama-C/Wp’s weak support for recursion.

the paper’s example of why order matters (Fig. 7 and Section 6.2, pp.18-19): in amax, the tool first writes the precondition n > 0 && \valid_read(a + (0 .. n-1)) for the access a[0], then a loop invariant for a[i] that depends on it. AutoSpec starts from the loop, a leaf in its graph, and the invariant it would need is discarded as unprovable because the precondition is not there yet.

Verus form. Inference: order agent work by reverse topological order of the crate’s call graph, and inside a function fix failing obligations top to bottom. Verus handles recursion with decreases, so the acyclic restriction is not imposed by the verifier, but the queue order and the termination argument of technique 6 would need rework for recursive functions.

technique 4: feed the unproved proof obligation back to the model

what it is: when a guard assertion is not proved, give the LLM the verifier’s proof obligation (assumptions and goal as the verifier encoded them), ask it to diagnose first, then to write specifications. The paper’s statement: “The feedback from a verifier, in particular, the proof obligations that remain to be discharged, can be leveraged to refine the specifications generated by LLMs effectively.” (Insight 2, p.8).

the paper’s worked example (Fig. 3 and Section 3.3, pp.7-8): search(arr, len, val) loops over arr[i]. With the precondition \valid_read(arr + (0..len-1)) the access is still unproved. The obligation shows two names for the array, arr_0 in the precondition and arr_1 at the access, and likewise len_0, len_1: the verifier assumes the loop may modify them. The missing fact is arr_0 == arr_1 and len_0 == len_1; the specification that provides it is loop assigns i.

how it is done: the obligation is a field of the prompt, and the prompt orders diagnosis before generation (Section 5.2.1, p.14): “Your tasks: (i) Diagnose the root cause of Frama-C/Wp’s failure to verify the assertion based on the provided feedback; (ii) Generate necessary specifications – such as preconditions, assigns clauses, and loop invariants – to enable successful verification.” A few annotated programs are included as examples.

evidence: the ablation (Fig. 8 and Section 6.4, pp.21-22) removes feedback-driven refinement (FDR), syntax correction (SC), or both. The text says disabling either one lowers the average V-Unit success rate, time and cost across most benchmarks, with SC the stronger effect when both are removed; Contiki is the exception, where the success rate rises, which the paper attributes to LLM uncertainty on a small module. Exact per-configuration numbers are only in the bar chart; the text gives 94.5% for Contiki with both removed, and says all ablated configurations stay above 83%. Inference: the ablation cannot rank this technique against the unit structure, which it never removes, and the effect of FDR alone on each benchmark is readable only from the chart.

Verus form. Inference: Verus does not print its verification conditions in a readable form; what it returns is the failed obligation, its source span and the clause that failed. So the prompt field would hold those, plus, for loops, a reminder of what Verus keeps across a loop: by default (loop isolation) a loop body does not use facts from outside it, even about variables the loop does not modify (AutoVerus paper §5: when loop isolation is false, Verus considers facts from outside a loop body inside it, and the default is true; #[verifier::loop_isolation(false)] turns it off). The paper’s specific fix, a loop assigns frame clause, has no Verus counterpart; the counterpart is restating in the invariant every outside fact the body needs, modified variable or not.

technique 5: split synthesis by role: host gets preconditions and invariants, callees get postconditions only

what it is: two separate LLM calls per refinement round, with different context and different permitted outputs (Sections 5.2.1-5.2.2, pp.14-15; Algorithm 1 lines 7-8, p.13).

how it is done:

1. host call: context is the host function alone with the already known properties; allowed outputs are preconditions, assigns clauses and loop invariants for the host. The call sites of the host are withheld on purpose: “Notably, the synthesis is strictly confined to the local context of function 𝑓 , excluding its call-site information to prevent over-constrained preconditions – a critical safeguard as illustrated in Section 3.2.” (p.14)
2. callee call: context is the host plus its direct callees; allowed outputs are postconditions and loop invariants of the callees; preconditions for callees are forbidden (pp.14-15)

why the split: a precondition written while looking at one caller tends to encode that caller’s use. The paper’s example (Fig. 2(d), p.7): seeing 1/x after x = id(1), an LLM may give id the precondition x != 0, which then fails at the unrelated call id(0). And a precondition differs in kind from other annotations (Remark, p.11): “Consequently, a violated precondition signals a potential RTE, whereas a violated postcondition or invariant is possibly invalid.”

the paper’s example (Fig. 6, p.14): for the division in one, the host call proposes requires x != 0 on one, which is ill-formed since one has no parameter x, and is dropped. The callee call proposes for id three postconditions: \result == x, \result != 0, and x != 0 ==> \result != 0. The second is false and is filtered out by technique 6; the other two prove the assertion.

Verus form. Inference: two prompts per failing obligation. Prompt A shows only the function containing the failure and may add requires, loop invariant and decreases to it, and proof hints such as assert. Prompt B shows that function and the callees’ bodies and may add only ensures to the callees (and invariants inside them). No prompt may add a requires to a function while its callers or its use at a call site are in view. This directly targets a known failure of agents: making a proof pass by a requires so strong that no real caller satisfies it.

limits: over-strong preconditions still occur. The paper’s Case 3 (Fig. 11, p.23): for reads of rate[0..2] the tool wrote \valid(rate + (0..2)), which demands writability of a constant array, where \valid_read was right.

technique 6: keep only what the verifier proves, except preconditions, which move up to callers

what it is: the acceptance rule for generated specifications (Section 5.2.3, p.15; Algorithm 1 lines 9-16, p.13).

how it is done:

1. syntax: an ill-formed candidate goes back to the LLM with the verifier’s error message, for a bounded number of attempts, then is dropped
2. semantics, non-preconditions: any generated postcondition, invariant or assigns clause the verifier cannot prove is deleted at once. The reason: “To prevent such false negatives, all unknown non-precondition specifications are discarded.” (p.15); an unproved invariant false would otherwise prove everything in the loop
3. semantics, preconditions: an unproved precondition is not deleted: “In contrast, an unknown precondition represents a guard assertion indicating a potential RTE (as discussed in Sections 3.1 and 3.2); it is thus retained in the V-Unit queue to be checked later at the corresponding call sites in caller functions.” (p.15)
4. loop: verify the guard assertion; if unknown, run the two calls of technique 5 and the checks above; repeat up to iter times (2 in the experiments, Section 6.1, p.17)
5. if the guard assertion is now proved: keep the new specifications, put the host’s new preconditions into the queued call-site units of its callers, and record the assertion and the non-precondition specifications as verified (lines 12-14)
6. otherwise add the guard assertion to the hypothesis set and continue as if it held (lines 15-16; steps ❼-❽ of Fig. 4)
7. at the end, return specifications, verified properties and hypotheses; a human reviews the hypotheses

why it terminates (Section 5.3, p.16): the queue’s length is fixed in phase 1 (number of RTE assertions plus number of call sites); a unit is never revisited (“Once a V-Unit is verified or marked as a hypothesis, its validity remains unchanged.”); new preconditions only affect units of callers, which lie later in the queue; each unit’s loop is bounded by iter.

what a hypothesis can be (Section 4, p.9): (a) a real error; (b) a false alarm the solver could not discharge; (c) a false alarm caused by an over-strong generated precondition; (d) a false alarm needing specifications beyond the tool’s reach.

Verus form. Inference: the same rule in Verus terms: after each generation round, delete every added ensures, invariant or assert that Verus does not prove, and never keep one alive with assume; keep an added requires and let Verus check it at callers; a failing obligation that survives the round budget is written to a human-facing list, and work continues on later functions with the unproved fact assumed. That last step would use an explicit, counted assume(...) at the failing point, and the final report must list every one. The list is the product: it tells a reviewer exactly which facts the proof of the rest depends on.

results

small programs (Frama-C-Problems, 51 programs averaging 17.43 lines; Claude Sonnet 4, temperature 0.7, iter = 2, three trials; Table 1, p.18). Num counts programs verified in at least one trial; Rate is the average success rate:

• “Overall, Preguss successfully verifies 46 out of 51 programs, achieving an average success rate of 79.7%, which substantially outperforms both AutoSpec (17/51, 32.7%) and AutoSpecRte (22/51, 41.8%).” (Section 6.2, p.18)
• by category for Preguss: General 12/12, Pointers 8/8, Loops 5/8 (rate 37.5%), Arrays 11/13 (69.2%), Arrays&Loops 5/5 (93.3%), Miscellaneous 5/5; the category counts sum to 46 and the category sizes to 51
• time for the whole suite: 65.59 minutes against 287.23 for AutoSpec; LLM cost $2.721against$0.448, about six times more; AutoSpec did not finish within 10 minutes on 28 of 51 programs (p.19)
• in this experiment all the RTE assertions are false alarms by construction: the paper says the stronger analyzer alone already proves these programs safe, so the weaker one is used to create targets (Remark, p.18)

real modules (Table 2, p.20; three trials each):

• Contiki AES-CCM* (544 lines, 10 functions): 163 RTE assertions, 182 V-Units, verified (181, 174, 162), average 94.7% (517 of 546, consistent); 111 reference specifications; a human changed (8, 15, 14) specifications afterwards, a reduction of 88.9% (1 − 37/333, consistent); 65.58 minutes, $1.77-X509-parserpolicymodule(1,199lines,20functions):142RTEassertions,174V-Units,verified(151,153,148),average86.6$3.84
• SAMCODE spacecraft control (1,280 lines, 48 functions): 44 RTE assertions, 133 V-Units, verified (121, 116, 119), average printed as 87.9%; 225 reference specifications; changed (34, 59, 38), reduction 80.6% (1 − 131/675, consistent); 80.48 minutes, $2.36-Atomthreadskernel(1,451lines,40functions):239RTEassertions,328V-Units,verified(252,258,258),average78.1$18.52
• the baselines typically did not finish within the 15-hour limit, producing fewer than 15 specifications or aborting, so they are not compared (Section 6.3, p.19)

errors found: “For the spacecraft control system SAMCODE, besides the 87.9% automatically verified V-Units, we identified 6 genuine RTEs (uninitialized left-value accesses) within the hypothesis set returned by Preguss.” (Section 6.3, p.20). They come from two logic bugs, confirmed by the developers. Case 2 (Fig. 10, p.23) shows how: the tool proved for GetUartData the postcondition that the buffer is initialized only when the return value is 1; the caller ignored the return value, so its read stayed unproved, and a human reading the proved postcondition saw why.

sensitivity (Appendix D, p.31): “Fig. 12 indicates no significant sensitivity of the V-Unit success rate to variations in iter, whereas execution time and inference cost exhibit a clear increasing trend with higher iter values.” Claude 4 gave a higher success rate, less time and lower cost than GPT-5; numbers are only in the charts.

a side result on hand-written specifications (Appendix C, p.30): X509-parser’s 251 reference specifications include 40 developer checkpoint assertions and 80 postconditions; Preguss generated 23, 17 and 35 postconditions in its three runs. The paper calls much of the reference set redundant for runtime-error freedom.

where the tool stops working

• data structures: “Preguss currently faces challenges in handling advanced specifications, such as inductive definitions and axioms [Blanchard 2020], which are especially crucial for verifying programs involving complex data structures like linked lists and trees (recall Atomthreads in RQ2).” (Section 7, p.24)
• loops needing complex or nested invariants: Loops category 5 of 8 with a 37.5% average rate (Table 1)
• library calls without source need hand contracts; most of the manual changes on Contiki were preconditions for memcpy and memset (Section 6.3, p.20)
• recursion is unsupported
• after a human weakens an over-strong precondition, properties proved under it may become unproved and must be removed (Section 6.3, p.21)

numbers and statements that do not fit together

• SAMCODE success rate: by the paper’s own formula, (121 + 116 + 119) / (3 × 133) = 356/399 = 89.2%, but Table 2 and the text print 87.9%. The other three rows match the formula. Either a count or the percentage is misprinted.
• the headline “reduction of 80.6%∼88.9% human verification effort” (Abstract, p.1) counts specifications a human touched divided by the size of a reference set; it is not time. For Contiki and SAMCODE the reference sets were written by the paper’s own experts within five person-days, and X509-parser’s reference set contains, by the paper’s Appendix C (p.30), 40 checkpoint assertions and many of its 80 postconditions that do not directly help validate guard assertions. Inference: this enlarges the denominator. The paper acknowledges a related gap for the success-rate metric: unverified units may need harder specifications than verified ones (Section 6.7, pp.23-24).
• two different success figures for the small suite: 46/51 is 90.2% but counts a program if any of three trials succeeded; 79.7% is the per-trial average. The abstract’s “substantially outperforms” rests on either.
• Inference: Algorithm 1 as printed adds to the hypothesis set only guard assertions that fail (line 16) and adds to the verified set the new specifications minus the preconditions (line 14). A generated precondition of a function that has no call site in the program therefore lands in neither set, while Lemma 22 (p.29) states that the analyzer’s assertions and the synthesized specifications together equal the verified set plus the hypothesis set. Example 12 (p.9) treats exactly such a precondition (search) as a hypothesis, so the intent is clear; the algorithm text does not do it.
• Algorithm 1 line 13 extracts preconditions from the accumulated set S, the prose (p.13) from the unit’s new set S′.
• the title’s 1001 lines: the two modules with full results above a thousand lines are 1,199 and 1,280 lines; the 1,451-line one was not completed.

already established here; VL need not repeat

• that the baseline AutoSpec, which is not guided by RTE assertions, typically did not finish within 15 hours on the four modules of 544 to 1,451 lines (Section 6.3); one baseline only
• the decomposition (one goal, host plus callees), the bottom-up order, the role split and the keep-only-proved rule, with a termination argument
• that a small refinement budget (2 rounds) is enough and more rounds mostly add cost
• that the leftover hypothesis list can hold genuine errors: 6 in one system, SAMCODE

Inference: not covered and still open for Verus work: functional specifications (the paper’s goals are generated by an analyzer, and it says precise functional properties remain hard to construct automatically, Section 5.4, p.16); recursive and data-structure-heavy code; any measurement of reviewer time.

relevance to VL as a threat

Inference: low as competition, high as method. The tool verifies existing C against a weak property (no runtime errors) and still leaves 5% to 22% of goals to a human; it does not produce functionally verified code. But its pipeline is the clearest published recipe for making LLM specification synthesis scale with program size, and its role split addresses the same over-strong-precondition problem that agent-written Verus contracts have. A competitor could port it to Verus quickly, since Verus already produces the goal list and the call-site checks.

techniques for the catalog

• alarm-guided specification synthesis: use each analyzer-reported possible runtime error as the property the LLM must make provable, not the function’s behaviour
• verification unit slicing: pair one guard assertion with its host function and direct callees as the whole context for one synthesis task
• placeholder call-site checks: create a precondition check at every call site up front with predicate true, so the work queue has fixed length before any contract exists
• bottom-up unit queue: process units of callees before callers and, within unrelated functions, by line number
• proof-obligation feedback with diagnose-then-generate prompt: give the LLM the verifier’s unproved obligation and make it explain the failure before writing annotations
• host/callee role split: generate preconditions and loop invariants only for the host without showing its callers, and only postconditions for callees
• discard-unproved rule: delete every generated non-precondition annotation the verifier cannot prove, so no unproved fact supports another proof
• precondition propagation: keep an unproved precondition and check it later at each caller’s call site, where failure marks a possible real error
• hypothesis set as output: record each goal that stays unproved, assume it, continue, and hand the list to a human as the residual review task
• bounded syntax repair: return ill-formed annotations to the LLM with the verifier’s error a fixed number of times, then drop them

Last edited: 2026-10-13