Specification synthesis, the task of automatically inferring formal specifications from program implementations and natural language, is important for refactoring, transpilation, optimization, and verification, yet remains an open challenge for large C++ repositories. Existing LLM-based approaches fail to simultaneously scale to such repositories, produce specifications expressive enough to capture systems-code features such as dynamic memory and heap-allocated data structures, and systematically validate those specifications to rule out incorrect candidates. We present Spec-Agent, an agentic system for synthesizing expressive, well-validated specifications across large C++ codebases. Spec-Agent targets a ladder of specification languages: propositional logic, first-order logic, propositional separation logic, and first-order separation logic. For each function, Spec-Agent uses static analysis and runtime heap tracing to select the appropriate target specification language, generalizes existing functional tests into fuzz harnesses, and iteratively refines LLM-generated candidates via counterexample-guided feedback. We evaluate Spec-Agent on open source C++ codebases comprising millions of lines of code. Spec-Agent synthesizes valid specifications for 85% of target functions, with no false positives observed under fuzzing and expert validation, outperforming Claude Code Opus 4.6 at 10x lower token cost.

翻译：规范合成——即从程序实现和自然语言中自动推断形式化规范的任务——对于重构、转译、优化和验证至关重要，然而在大型C++代码仓库中仍是一个开放性挑战。现有基于大语言模型的方法无法同时满足以下需求：扩展到此类代码仓库、生成足以描述系统代码特征（如动态内存和堆分配数据结构）的表达性规范、以及系统化验证这些规范以剔除错误候选。我们提出Spec-Agent，一个面向大型C++代码库、用于合成表达性强且经过充分验证的规范的智能体系统。Spec-Agent针对一系列规范语言：命题逻辑、一阶逻辑、命题分离逻辑和一阶分离逻辑。对于每个函数，Spec-Agent通过静态分析和运行时堆追踪选择合适的规范语言目标，将现有功能测试泛化为模糊测试工具，并通过反例引导的反馈迭代优化LLM生成的候选规范。我们在包含数百万行代码的开源C++代码库上评估了Spec-Agent。Spec-Agent为85%的目标函数合成了有效规范，在模糊测试和专家验证下未观察到误报，性能优于Claude Code Opus 4.6的同时将代币消耗降低了10倍。