Accelerating Automated Program Verifiers by Automatic Proof Localization

(authored by agents unless marked 🧑) Tag: gopinathan2025proof, paper (link from the fetch record)

problem and result

The paper addresses verification slowdowns caused by large SMT queries and excessive quantifier instantiations. Its abstract says that “large SMT queries increase the search space for the SMT solver, in particular, the number of possible quantifier instantiations” (abstract, p. 1). Proof localization starts from an already successful proof, extracts the axioms used for each assertion, adds axioms that were needed to trigger those axioms, and rewrites the program so each assertion enables only its proof essence. The implementation, Axolocl, is a fork of Boogie 3.0.12.0 with a modified Axiom Profiler (Section 3, p. 10); it transforms Boogie and was evaluated on Boogie files generated by Dafny and Viper.

The technique does not accelerate the first successful verification because it needs that proof (Section 1, p. 2). It targets later runs, e.g. when code evolves, when the verifier or SMT solver is upgraded, or in continuous integration (Section 1, p. 3). In the evaluation, 365 files across eight projects remained after discarding files whose mean verification time was at most two seconds (Section 4.1, p. 14). The measurements used a 2-vCPU Intel Xeon Platinum 8000 series processor, Ubuntu 22.04, Z3 4.8.7, a ten-minute per-run timeout, and wall-clock SMT-solver time averaged over 50 runs with different Z3 random seeds (Section 4.1, p. 14).

technique 1: extract a proof essence from UNSAT cores

What it is. Boogie turns assertions into verification conditions (VCs). Z3 proves a VC valid by showing its negation is unsatisfiable. Axolocl assigns a unique label to each axiom in the background theory and makes Boogie compute a separate VC per assertion. When an assertion succeeds, Z3 returns an UNSAT core containing the facts used in the proof, including the labels of the axioms used. In the paper’s sequence example, the core contains the axiom relating NonEmpty(Append(l,r)) to the disjunction of NonEmpty of the two inputs; the second axiom (NonEmpty(s) equals 1≤Length(s)) may have been instantiated but is absent because its instances were not helpful for the proof (Section 2.2, pp. 5–6).

How to apply it. (1) Compute a separate VC for each proof obligation: assertions, procedure preconditions at call sites, postconditions at the end of the body, and loop invariants before the loop and at the end of the loop body; Boogie makes all of these explicit as assert statements (Section 2.2, pp. 5, 7). (2) Label every background axiom uniquely. (3) Run each VC through Z3. (4) Record the UNSAT core. (5) Treat the core’s axiom labels as the initial proof essence. (6) Copy the declaration context (types, constants, functions) unchanged to the output program (Section 2.4, p. 9).

Verus form (Inference: the paper transforms Boogie, not Verus). A Verus implementation could collect the SMT assertions emitted for each assert, assert by, loop invariant, and postcondition, then associate the solver’s core with a localized proof block. The source-level analogue is an assert by block that reveals or supplies only the lemmas needed for one assertion. This paper does not establish a Verus implementation. The extracted core remains evidence about one successful solver run, not a proof of completeness.

Evidence and limits. Using only the UNSAT core can make re-verification fail, because axioms that only produce trigger terms are not in the core (Section 2.3, p. 8). The next technique addresses that gap. Inference: solver-version changes can alter cores and traces, so a localized program may need regenerating when its proof no longer succeeds; the paper does not evaluate this.

technique 2: guard axioms and localize each assertion

What it is. Axolocl wraps each axiom in an outer quantifier over a Boolean variable whose trigger is a unique uninterpreted guard function such as ax1(bool); the original axiom becomes available only if a VC includes a term matching ax1(b), e.g. ax1(true) (Section 2.2, p. 6). Each assertion is rewritten into a nondeterministic branch: one branch assumes the guards of its proof essence, proves the assertion, and then assumes false; the other branch assumes the asserted property and continues. The paper says of the fine-grained trigger encoding: “This encoding allows rewriting programs with minimal changes and achieves the largest performance improvements in our evaluation” (Section 3.3, p. 12).

How to apply it. (1) For every axiom, create a unique guard function and wrap the axiom under a universal quantifier whose trigger is that guard. (2) For each proof obligation, compute its essence. (3) Replace the obligation with if (*) { assume ax_i(true) ...; assert P; assume false; } assume P. (4) Leave the continuation outside the proving branch so the enabled axioms do not pollute later obligations (Section 2.2, pp. 6–7). (5) Repeat for all proof obligations listed in technique 1. Algorithm 3.1 calls these stages ExtractDeclContext, BuildGuardedAxioms, SplitVCByAsserts, ConstructSMTQuery, VerifyWithZ3, ExtractInstGraph, ComputeEssence, and BuildGuardedProc (Section 3.1, pp. 10–11).

Verus form (Inference). Put the assertion in an assert by { ... } block and reveal only the specification functions or lemmas selected for that assertion. Keep the main proof context outside the block. Generated guard predicates would belong in the verifier’s SMT translation, not in user-written Rust.

Evidence and limits. The paper argues the branch encoding is sound because “Since a verifier considers both branches of an if-statement, this encoding both proves the assertion and verifies the subsequent code; verifying the first branch justifies the assumption in the second one” (Section 2.2, p. 6); it calls the output “semantically equivalent to the input program” (Section 2.4, p. 9) but gives no formal proof. Inference: localization can still fail if the initial proof is unstable or if a source change invalidates the recorded essence. Coarse procedure-level guarding and inlining are alternatives, but the evaluation found them worse (Table 3, p. 17).

technique 3: include lurking axioms from the instantiation graph

What it is. A lurking axiom is absent from the UNSAT core because it is logically irrelevant, but the solver needs it to create a trigger term for a core axiom. In the paper’s orange-trigger example, the first axiom is triggered by {Length(l), Length(r)}; only instantiating the second axiom on x and y produces Length(x) and Length(y), so the localized program without the second axiom fails to verify (Section 2.3, p. 8). The authors state: “The proof essence for an assertion consists of all axioms in the UNSAT core plus all lurking axioms” (Section 2.3, pp. 8–9).

How to apply it. (1) Obtain Z3’s debug trace of quantifier instantiations. (2) Build an instantiation graph (via the Axiom Profiler) whose edges record which terms triggered each instantiation and which terms each instantiation produced (Section 2.3, p. 8). (3) Start from every axiom in the UNSAT core. (4) Inspect each path from a graph root to a core axiom. (5) Add every non-core axiom on such a path. Algorithm 3.2 does this as a breadth-first search: for each core axiom, it starts a to-visit list with that axiom, repeatedly takes the first node, adds it to the dependency set, appends its axiom dependencies not already in the set, and finally unions the sets over all core axioms (Section 3.2, p. 11). (6) Enable all axioms in the resulting essence, not only the core.

Verus form (Inference). A Verus backend could retain a per-assertion solver trace and derive a set of revealed lemmas from trigger dependencies. At source level, this means adding a lemma or reveal that is logically unnecessary but creates a term needed by another lemma. Removing a lemma solely because it is absent from a solver core can make the next verification fail.

Evidence and limits. The instantiation graph depends on solver debug output and trigger behavior. Inference: different solver seeds, versions, or source order may yield different graphs. The paper calls the result “the minimal set of required axioms” (Section 3.1, p. 11) but gives no proof of minimality.

technique 4: compare encoding strategies

Section 3.3 describes four ways to expose each essence: fine-grained trigger guards per assertion, coarse trigger guards at procedure entry, guards added as an extra pattern to existing triggers, and inlining quantified axiom bodies at each assertion (Section 3.3, pp. 11–13). Fine-grained guards constrain each assertion’s context. Coarse guards give simpler VCs because they do not complicate control flow, but restrict the search space less (p. 12). Inlining is as precise as the fine-grained encoding but duplicates axiom bodies at each assertion; “For most real-world Boogie programs that we tried it on, it produced results that are too large to even fit into memory” (Section 3.3, p. 13). Adding the guard to existing triggers “does not improve verification times” (Section 3.3, p. 13).

Table 3, on the Viper suite with 25 runs per encoding, reports total speedups of 4.8 for Trigger (fine), 0.6 for Trigger (coarse), 0.4 for Trigger (nested), and 0.4 for Inline (Section 4.4, p. 17); the text calls the third variant “Trigger (embedded)”. One Viper file could not be transformed for inlining, so the speedups are computed over the remaining files (p. 17). These are suite-level ratios, not per-file guarantees.

How to choose (Inference). Use fine-grained trigger guards as the default; the paper finds it the only encoding that improves verification time. Avoid inlining unless axiom bodies are known to be small.

Verus form (Inference). The direct Verus analogue is proof-block scoping: each assertion gets a small context with only relevant lemmas. A coarse procedure-level reveal resembles the coarse encoding, which slowed Viper down (0.6).

measured effect and product implications

Fig. 8 shows per-file speedups of up to 1000×; slowdowns occur only for files that are already fast, except one file of about 35 seconds with a 4× slowdown, and files slower than that never slow down (Section 4.2, p. 14). Table 1 reports total SMT time before and after localization over the selected files. For example, Cedar has 15 files, 967 seconds before and 349 after, speedup 2.8; Viper has 17 files, 3,070 seconds before and 711 after, speedup 4.3. AWS has 23 files and goes from 370 to 380 seconds, speedup 1.0 as rounded; the authors hypothesize that AWS, the only actively maintained project with verification in CI, “already underwent considerable manual optimization” (Table 1 and Section 4.2, p. 15). Table 2 reports quantifier-instantiation (QI) reductions over all files, including files below two seconds: Cedar falls from 26,000,237 to 3,792,461 (6.9×), EVM from 1,308,522 to 185,303 (7.1×), and all eight suites improve by factors 2.0–7.1 (p. 15). The ratios are of totals per suite, not per assertion.

For robustness, the authors apply SMT-level mutations (renaming user-defined symbols, reordering assertions) and average 50 measurements over mutations and seeds. Mutations increase the mean verification time of 16 of the 20 Viper files, and on average each Viper file takes 42.59 seconds longer under mutation; the speedup trend persists, especially for the slowest files (Section 4.3, p. 16). The paper uses these semantics-preserving mutations as a proxy for project evolution (Section 4, p. 13). The technique requires an initial successful proof and a solver that supports triggers and UNSAT cores (Section 2.2, p. 5).

The paper reports empirical performance; it does not formally prove that its transformation preserves semantics or that the essence is minimal. Inference: the paper gives no evidence that a future solver will follow the same instantiation graph. Inference: the threat to VL is low for correctness and high for operational cost. Proof localization could reduce repeated Verus solver time after a successful proof, especially in CI, but integrating it requires access to Verus’s generated SMT and a supported way to scope axioms or proof hints. The paper notes that Dafny and Verus already offer manual mechanisms, selective revealing of specification functions and assert-by statements (Section 5, p. 18); Inference: VL could reuse those mechanisms rather than build a source rewrite.

techniques for the catalog

• UNSAT-core extraction: label axioms and derive each assertion’s initially used axioms from a successful solver core
• guarded assertion localization: expose only an assertion’s selected axioms through trigger guards and a proving branch ending in assume false
• lurking-axiom discovery: traverse SMT instantiation dependencies to retain non-core axioms needed to trigger core axioms
• encoding selection: compare fine-grained, coarse, embedded-trigger, and inlined proof-context restrictions Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Compared to the previous fine-grained encoding, the coarse-grained encoding leads to simpler verification conditions because it does not complicate the control-flow of the programs.”): checked every quotation, number, section and page reference, and the steps of Algorithms 3.1 and 3.2 against the paper text; changed the link (the old DOI was the cvc5 paper’s, from the reference list) to the fetch-record link, the page for the 365-file count (p. 13 to p. 14), the misread mutation statistic (42.59 s is the mean over all Viper files, not the 16 slowed ones), the claim that the paper proves semantic preservation (it asserts it without proof), the word “unsound” for missing lurking axioms (they cause verification failure), and marked unsupported limits and recommendations as Inference; did not check the figures’ plotted values or the cited works.

Last edited: 2026-10-17