SpecAgent：用智能体框架自动合成 C 程序形式化规约
SpecAgent: Empowering Program Verification with Agentic Synthesis of Formal Program Specifications
写 C 程序验证的朋友可以看看，这个 SpecAgent 会自己排查依赖再修规约，811 个目标里证出 604 个，比已有基线强不少。
程序验证需要形式化规约，但人工编写成本高，现有 LLM 方法多采用单向生成加局部修复，遇到函数与循环间的复杂依赖时容易产生级联失败。论文提出 SpecAgent 智能体框架，包含依赖感知规划、RAG 检索规约模式、智能体修复和智能体批判四个组件。在来自 14 个真实仓库的 50 个程序上，SpecAgent 配合 DeepSeek-V4 合成规约的精确率达 96.82%、召回率达 88.95%，超过所有基线。在 811 个真实验证目标上成功证出 604 个，同样领先现有方法。
SpecAgent: Empowering Program Verification with Agentic Synthesis of Formal Program Specifications
Formal specifications are essential for deductive program verification, providing semantic abstractions for compositional verification of complex software. However, manually constructing specifications is labor-intensive, motivating automated synthesis. Despite recent advances in large language models (LLMs), existing approaches often rely on forward-only workflows and localized repair, limiting their effectiveness on real-world programs with complex dependencies among functions and loops. Verification failures may stem from previously generated specifications, causing cascading failures that local refinement cannot resolve. To address these challenges, we present SpecAgent, an agentic framework for synthesizing high-quality ACSL specifications for real-world C programs. SpecAgent integrates four components: dependency-aware planning to identify specification targets, retrieval-augmented generation (RAG) to provide relevant specification patterns and program context, agentic repair to diagnose defects and revisit dependent specifications, and agentic critique to assess and refine semantic strength beyond proof success. We evaluate SpecAgent on specification synthesis and program verification tasks. On 50 programs from 14 real-world repositories, SpecAgent with DeepSeek-V4 achieves 96.82% precision and 88.95% recall in synthesizing correct and strong specifications, outperforming all baselines. On 811 real-world verification targets, it successfully discharges 604, also surpassing existing baselines. These results demonstrate SpecAgent's effectiveness in synthesizing high-quality specifications and facilitating real-world program verification.
