VERDICT: Multi-Agent Parallel Modular Verification

I. INTRODUCTION

• Earlier LLM-based approaches use localized verification units to manage context, but validate them bottom-up, callees before callers.The cited approaches include PREGUSS and SpecSyn.Source: §I · p. 1
• Bottom-up synthesis limits parallelism across call levels and lacks a systematic way to reconcile contract conflicts that can propagate through call chains.A callee contract change can invalidate caller proof obligations and trigger further revisions across transitive callers.Source: §I · p. 1
• On 15 real-world benchmarks, VERDICT outperforms PREGUSS and SpecSyn in specification quality and verification time, and verifies the complete X.509 parser with over 20,000 lines of code in a few hours.The paper describes the X.509 task as previously requiring months of expert manual effort.Source: §I · p. 2
• VERDICT replaces sequential bottom-up synthesis with assumption-based parallel dispatch and event-driven bidirectional reconciliation.Each function agent can proceed using assumed contracts for unresolved callees; Supply events propagate callee changes upward, while Demand events carry caller requests downward.Source: §I · pp. 1–2

A. Modular Verification

• A function contract abstracts its implementation through preconditions and postconditions, so a verified function can be replaced at each call by its contract.For example, reverse uses swap’s contract at the call site without re-examining swap’s body.Source: A. Modular Verification · p. 2

B. Proof Goals

• Proof goals are assertion-encoded program properties that are discharged only when the assertion and all specifications it depends on are jointly proved.The array-reversal assertion, for example, depends on reverse’s postconditions.Source: B. Proof Goals · pp. 2–3

C. Bottom-up Verification Paradigm

• Bottom-up verification constructs specifications for leaf functions first, then propagates verified contracts upward because callers depend on established callee contracts.In the example, swap is verified before reverse, and reverse before main.Source: C. Bottom-up Verification Paradigm · p. 3

A. Assumption-Based Parallel Specification Synthesis

• Bottom-up verification requires swap to finish before reverse and reverse before main, leaving higher call levels idle while lower-level verification proceeds.Specification generation and FRAMA-C/WP validation are tightly interleaved within each unit’s guess-and-check cycle.Source: A. Assumption-Based Parallel… · p. 3
• VERDICT assigns each function an agent that can verify under assumed callee contracts, allowing functions across call levels to begin concurrently.Each agent generates assumptions from callee bodies and call-site contexts, then constructs and publishes its own specifications.Source: A. Assumption-Based Parallel… · p. 3

B. Bidirectional Interprocedural Conflicts Reconcilation

• Interprocedural conflicts arise when a caller needs a stronger callee postcondition or weaker callee precondition, or must strengthen its own precondition.These deficiencies can originate elsewhere in the call chain rather than in the function whose proof fails.Source: B. Bidirectional Interprocedural… · p. 3
• The three conflict forms can interleave across the call graph, requiring contract revisions both downward to callees and upward to callers.A stronger postcondition may require a stronger precondition that cascades upward, while an overly aggressive precondition can trigger a neighboring precondition conflict.Source: B. Bidirectional Interprocedural… · p. 4
• Bottom-up approaches lack both caller-to-callee refinement and a way to propagate repairs across arbitrarily many call levels.The figure examples illustrate demands to strengthen a callee’s postcondition, weaken its precondition, and strengthen a caller’s precondition with an upward cascade.Source: B. Bidirectional Interprocedural… · p. 4, Figure 3 · p. 4, Figure 4 · p. 4

• Each function has a persistent agent that owns its specification and begins verification under assumed contracts for unpublished callees.This design is intended to remove ordering constraints while supporting parallelism.Source: §IV · p. 4
• A runtime orchestrator coordinates agents using Event Supply for upward cascades and Event Demand for downward requests.Source: §IV · p. 4
• Each agent follows a four-state machine whose transitions are triggered exclusively by events.Together, the agents and orchestrator provide infrastructure for bidirectional conflict reconciliation.Source: §IV · p. 4

A. Agent Dispatch

• Each V-Unit pairs a host function with its direct callees, and one agent exclusively owns the host’s writable contract and intraprocedural specifications.Exclusive ownership routes revision requests to a single agent rather than allowing concurrent callers to modify the same contract.Source: A. Agent Dispatch · p. 5

B. Assumption-Based Verification

• When a callee has not published a contract, its agent constructs a provisional assumption from the callee’s body and proceeds with host verification.Source: B. Assumption-Based Verification · p. 5
• An agent generates ACSL annotations and uses FRAMA-C/WP to check host proof goals, specification clauses, and callee preconditions at call sites.Source: B. Assumption-Based Verification · p. 5

C. Event-Driven Bidirectional Reconciliation

• A Supply event prompts callers to re-verify against a callee’s new contract, while a Demand event asks a callee to prove a caller’s requested property.A callee incorporates and publishes the requested property if its implementation supports it.Source: C. Event-Driven Bidirectional… · p. 5
• When a conflict persists, an agent may revise its own precondition upward or demand changes from its callees downward, after first attempting an intraprocedural fix.These options are non-exclusive, and the resulting events can trigger further revisions in either direction across the call graph.Source: C. Event-Driven Bidirectional… · p. 5

A. Agent State Machine

• Agents move among WORK, IDLE, WAIT, and TERM as they verify, await events, enter the queue, or exit scheduling.Source: A. Agent State Machine · p. 5
• The orchestrator dispatches waiting agents when a concurrency slot opens, while max_cycles limits each agent’s permitted WORK rounds.If the concurrency pool is full, an agent remains in WAIT; exhausting its cycle budget moves it to TERM.Source: A. Agent State Machine · p. 5

B. Scheduling Procedure

• Agents are enqueued in reverse topological order so deeper callees run first when concurrency is limited, reducing the number of revivals intuitively.Source: B. Scheduling Procedure · p. 5
• In the nine-step example, agents first run concurrently, then events revive only affected agents while an agent without conflicts remains idle.After the second reconciliation, no further events arise; all agents are idle and the orchestrator terminates.Source: B. Scheduling Procedure · p. 6

C. Termination of the Orchestrator

• Finite cycle budgets and WORK-round time limits ensure every agent eventually becomes idle or permanently terminates.The orchestrator terminates when only idle or terminated agents remain with no events, or when all agents have terminated.Source: C. Termination of the Orchestrator · p. 6

D. Soundness of the Orchestrator

• For any subgraph, converged agents imply valid proof goals when the preconditions of its entry functions are satisfied.An agent converges when it is idle, all tracked obligations are discharged, and no pending event targets it.Source: D. Soundness of the Orchestrator · p. 6

VII. EVALUATION

• The evaluation poses three questions on baseline comparison, scheduling hyper-parameters, and the contributions of VERDICT’s two mechanisms.RQ1’s table covers specification quality and verification time; the evaluation describes overall rates across benchmarks and geometric-mean time.Source: §VII · pp. 6–7, Table I · p. 7

Implementation

• VERDICT uses asyncio-based concurrency with FRAMA-C/WP and the Z3, cvc5, and Alt-Ergo solvers.The implementation is built on the Claude Agent SDK.Source: A. Experimental Setup · p. 7

Models and configurations

• Experiments use Claude Sonnet 4.6 and Opus 4.5, with max_parallel = 8 and max_cycles = 24 by default.The x509-parser-full benchmark uses max_parallel = 16; RQ1 runs three repetitions, while RQ2 and RQ3 use one trial with both models.Source: A. Experimental Setup · p. 7

Baselines and benchmarks

• VERDICT is compared with PREGUSS and SpecSyn, both bottom-up tools run with the same LLMs for fairness.Benchmarks drawn from the tools’ evaluation corpora exclude trivial-size cases and atomthreads, whose inductive-predicate needs are outside scope, and add two ANSSI X.509 parser modules.Source: A. Experimental Setup · p. 7

Metrics

• FRAMA-C/WP reports discharged runtime-error and tool-generated specification goals, alongside end-to-end wall-clock time.The 15 benchmarks span 7 to 210 functions and call-chain depths of 0 to 16; each tool’s rates and time are reported as mean±std over three repetitions, with overall rates and geometric-mean time.Source: A. Experimental Setup · p. 7

B. RQ1: Comparison against Baselines

• 99.9% on rte and 94.5% on spec (Opus): VERDICT exceeds PREGUSS at 89.8%/75.3% and SpecSyn at 72.5%/84.7%.VERDICT also surpasses each baseline on its own stronger dimension: PREGUSS’s rte and SpecSyn’s spec.Source: B. RQ1: Comparison against Baselines · pp. 7–8
• 12 minutes: VERDICT’s geometric-mean verification time with Opus, versus 25 minutes for PREGUSS and 81 minutes for SpecSyn.VERDICT is most efficient on 12 of 15 benchmarks, and its speed advantage grows with program size and call-chain depth.Source: B. RQ1: Comparison against Baselines · p. 8
• 20,000-line X.509 parser: VERDICT proves the near-complete absence of runtime errors in a few hours, while manual verification required months of expert effort.The paper identifies this as the first automated approach to achieve this scale of verification.Source: B. RQ1: Comparison against Baselines · p. 8

C. RQ2: Effects of the Scheduling Parameters

• 4.9×: geometric-mean parallel speedup across six benchmarks at mp=32; Opus reaches 11.9× on hypatia.Speedup grows as max_parallel increases, but remains below ideal linear scaling; more parallelism also increases reconciliation overhead.Source: 1) max_parallel · p. 8
• 19× to 7×: on x509-parser-2, reconciliation reduces the initial-dispatch potential speedup to the eventual speedup at mp=32.On hypatia, with less interdependence, the eventual speedup reaches 12×; reconciliation resolves conflicts that ripple through deep call chains.Source: Figure 8 · p. 8, 1) max_parallel · p. 8
• ≈90% to ≈99%: mean spec discharge rises by mc≈8, while deep-chain X.509 convergence reaches its maximum by about eight cycles.Shallow-chain benchmarks saturate earlier, by about two to four cycles.Source: 2) max_cycles · p. 9, Figure 9 · p. 9

D. RQ3: Contribution of Individual Mechanisms

• Event Supply remains enabled in every ablation because it triggers re-verification when a callee publishes a new contract, preserving soundness.Source: D. RQ3: Contribution of Individual… · p. 9
• Near-perfect quality on the four shallow programs is largely unchanged across the ablation configurations.These are contiki, hypatia, voronoi, and sokol, all with call-chain depth at most four.Source: Figure 10 · p. 9, D. RQ3: Contribution of Individual… · p. 9
• 99.7% to 81% (Opus) and 84% (Sonnet): removing Event Demand lowers deep-chain specification discharge.Without Event Demand, agents cannot ask callees to repair cross-level conflicts; the no-both configuration gives similar outcomes.Source: Figure 10 · p. 9, D. RQ3: Contribution of Individual… · p. 9
• 28 to 49 Demand Events (Opus) and 11 to 48 (Sonnet): removing assumed contracts sharply increases demands on deep-chain programs while quality stays above 99%.Without optimistic assumptions for unpublished callees, dependencies must be resolved sequentially through Event Demands.Source: Figure 10 · p. 9, D. RQ3: Contribution of Individual… · p. 9
• Event Demand safeguards quality, while assumed contracts deliver efficiency; neither can be removed on deep, intricate call structures without loss.On shallow programs, both mechanisms are neutral, consistent with reconciliation being engaged only when conflicts arise.Source: D. RQ3: Contribution of Individual… · p. 9

E. Threats to Validity

• Specification quality is the fraction of proof goals discharged under a unified external FRAMA-C/WP configuration.The authors consider manual refinement to 100% discharge more rigorous, but prohibitively expensive on the most informative benchmarks.Source: E. Threats to Validity · pp. 9–10
• On benchmarks already at 100% discharge, VERDICT leads on 12 of 15 rte benchmarks, versus 6 for PREGUSS and 3 for SpecSyn.Because no human intervention is required for this subset, the comparison also holds where the discharge metric entails no refinement work.Source: E. Threats to Validity · p. 10
• The authors treat discharge rate as a proxy for refinement effort because tools that discharge more goals leave arguably less work for manual refinement.They did not manually refine specifications on x509-parser-full, where both baselines leave substantial numbers of goals undischarged.Source: E. Threats to Validity · p. 10

VIII. LIMITATIONS AND FUTURE DIRECTIONS

• Synchronous reconciliation rounds leave revived agents waiting for round boundaries, contributing to the gap between eventual and ideal speedup.Resuming agents immediately upon their triggering events could overlap consecutive rounds and reduce this tail effect.Source: §VIII · p. 10
• Function-level agents improve parallelism and limit context size, but tightly coupled functions incur more renegotiation and tail latency.The open partitioning problem balances parallelism, coordination overhead, and per-agent context size; grouping tightly coupled functions such as an SCC is an alternative.Source: §VIII · p. 10
• VERDICT and the baselines target RTE absence, while recursive unbounded structures may require inductive predicates and lemmas that remain challenging for current LLM-based synthesis.Supporting those artifacts could broaden the properties VERDICT certifies.Source: §VIII · p. 10

IX. RELATED WORK

• LLM specification-synthesis systems commonly use guess-and-check: a verifier checks candidate specifications and failures guide iterative refinement.The paper describes this as a recent line of work aimed at automating deductive verification.Source: §IX · p. 10
• Most surveyed systems target single functions and remain limited to shallow or absent call dependencies despite strong per-function success rates.The paper includes AutoSpec, SLD-Spec, SpecGen, Laurel, LORIS, AutoVerus, and Msg among these systems.Source: §IX · p. 10
• PREGUSS and SpecSyn use bounded, bottom-up units, which prevent cross-boundary specification demands and interleaved conflict reconciliation across call levels.VERDICT addresses these limits with assumption-based verification and bidirectional interprocedural reconciliation.Source: §IX · p. 10
• FM-Agent generates specifications top-down for bug finding against natural-language specifications, rather than for deductive verification.The paper therefore does not treat it as a baseline.Source: §IX · p. 10

X. CONCLUSION

• VERDICT enables almost fully automated RTE-freeness verification of real-world programs over 20,000 LoC, beyond the roughly 1,000-LoC scale previously reported.The conclusion also reports substantial improvements over state-of-the-art baselines in specification quality and efficiency.Source: §X · p. 11