Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.29147

VERDICT: Multi-Agent Parallel Modular Verification

Tengjie Lin·Zhongyi Wang·Haokun Li·Jianwei Yin·Mingshuai Chen
View original source ↗Read source document ↗Export metadata ↓

Abstract

Deductive verification scales to large software systems through modular reasoning, where formal contracts summarize the behavior of individual functions and enable their independent verification. Its central bottleneck is specification synthesis: constructing the contracts required for modular verification. Recent advances in large language models (LLMs) have enabled automated specification synthesis at unprecedented scale. However, existing approaches remain fundamentally bottom-up, requiring callees to be verified before their callers. This dependency limits parallelism and provides no principled mechanism for resolving interprocedural inconsistencies that propagate across call chains. We present VERDICT, a multi-agent framework for parallelizing modular deductive verification of large-scale programs. VERDICT is built on two key principles. First, assumption-based parallel specification synthesis assigns an agent to each function and allows it to proceed immediately using assumed contracts for its callees, enabling verification to proceed in parallel across the program. Second, bidirectional interprocedural conflict reconciliation resolves the inconsistencies introduced by these assumptions: when a synthesized contract contradicts an assumption, agents propagate the necessary revisions both up and down the call graph until the contracts converge. Experimental results on real-world C programs show that VERDICT synthesizes higher-quality specifications than existing approaches while substantially reducing verification time. In particular, VERDICT is the first approach that scales to the complete 20,000-line X.509 parser, ruling out nearly all the potential runtime errors within hours, whereas prior tools like PREGUSS fall far short even after days of execution.

Explore related subjects

cs.SEcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Tengjie Lin, Zhongyi Wang, Haokun Li, Jianwei Yin, Mingshuai Chen. 2026-10-21. VERDICT: Multi-Agent Parallel Modular Verification. https://arxiv.org/abs/2610.29147

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Generating Mitigations for Downstream Projects to Neutralize Upstream Library Vulnerability

Third-party libraries are essential in software development as they prevent the need for developers to recreate existing functionalities. However, vulnerabilities within these libraries pose significant risks to dependent projects. Upgrading dependencies is infeasible when no patched version is available or when downstream projects have strict version constraints. Moreover, repairing the vulnerability proves challenging when the source code of the library is inaccessible. State-of-the-art automatic vulnerability repair and automatic program repair methods both fail to address this issue. Therefore, mitigating library vulnerabilities without access to source code or available patches is crucial for a swift response to potential security attacks. Existing tools encounter challenges concerning generalizability and functional security. Upon vulnerability disclosure, LUMEN prepares a pool of candidate mitigation strategies by retrieving explicit workarounds from public sources and supplementing the pool with generated strategies based on vulnerability reproduction behavior. LUMEN then selects a suitable strategy, autonomously gathers repository-specific context, and adaptively generates a validated mitigation patch. We evaluate LUMEN on 474 impacted functions associated with 94 vulnerabilities. LUMEN successfully mitigates 393 functions, achieving a success rate of 82.91%, which substantially outperforms the adapted baseline in blocking vulnerability reproduction under our exploit-based evaluation. Additionally, our ablation study evaluates the contributions of strategy composition, strategy selection, and repository-level context collection. Further evaluations show that LUMEN can mitigate vulnerabilities disclosed after the knowledge cutoff of the base model.

cs.SE↗
arXiv2026

MockingBird: Context-aware Repository-level Code Translation with Isolated Validation

Despite advances in repository-level code translation, automated type resolution across differing type systems and translation validation (functional-equivalence checking) remain challenging. This paper proposes MockingBird, combining context-aware type resolution with mock-based isolated validation. MockingBird retrieves API documentation and contextual code information per source-language type, prompting an LLM to resolve precise cross-language type mappings, reducing the manual effort of existing approaches. Using this automatically constructed type map, MockingBird employs custom serialization/deserialization to generate equivalent target-language mock objects, validating each translation unit in isolation without test translation, eliminating test-overfitting risks and translation challenges. On 10 Java-to-Python tasks from the AlphaTrans benchmark, MockingBird improves functional equivalence from the state-of-the-art 25.14% to 43.10%, with no manual type-mapping correction needed. A 700-fragment study shows MockingBird achieves 0 false positives and 0.9% false negatives, substantially outperforming GraalVM (2.4% false positives, 7.6% false negatives) and MatchFixAgent (11.0% combined mislabel rate). The pipeline is also LLM-agnostic, maintaining these gains with both DeepSeekCoder-33B and the smaller Devstral-24B.

cs.SE↗
arXiv2026

Learning from Repair Experience: Self-Evolving Agents for Automated Vulnerability Repair

Large Language Models (LLMs) have shown promise for automated vulnerability repair (AVR), but they still face several limitations, including the lack of intra-vulnerability experience accumulation and the lack of cross-vulnerability experience reuse. As a result, LLMs may repeatedly make similar mistakes during iterative repair and underutilize valuable repair knowledge from historical vulnerabilities. To address these challenges, we propose EvoRepair, an experience-based self-evolving AVR agent framework that enables LLMs to accumulate, refine, and leverage domain-specific knowledge across long-horizon vulnerability repairs. EvoRepair follows a cyclic learn-and-repair process that retrieves relevant past experiences to guide repair, extracts new experiences from repair trajectories, and updates an experience bank using quality-aware scoring. We evaluate EvoRepair against 15 representative vulnerability repair baselines on PATCHEVAL and SEC-bench. Results show that EvoRepair achieves the best overall performance, reaching 93.47% on PATCHEVAL, 87.00% on SEC-bench, and 90.46% overall. In particular, EvoRepair outperforms the latest LLM-based baseline LoopRepair by 39.56% and 33.50% on PATCHEVAL and SEC-bench, respectively, and surpasses IntentFix by 70.86% and 50.50%. Across both benchmarks, EvoRepair also exceeds the recent self-evolving agent Live-SWE-Agent by 6.98% overall. Additional transfer experiments on VUL4J further demonstrate the robustness of EvoRepair across models, programming languages, and datasets. These findings demonstrate that experience-based self-evolution substantially strengthens agentic AVR and goes beyond existing self-evolving techniques.

cs.SE↗