一句话：首个工业级工具，引导 LLM 合成带量词的一阶逻辑 C++ 规范，准确率达 85%。
本文提出 Fun2spec，首个工业级、面向大规模 C++ 代码的代码契约合成工具。其核心思路是引导大语言模型（LLM）生成一阶逻辑（含量词）形式的 C++ 规范，并通过自动化验证流程配合错误驱动的 oracle 反馈来迭代修正，从而保证规范的语义正确性。在标准基准上，Fun2spec 达到 85% 的准确率，且能在 60% 的情况下生成最强代码契约，相比先前方法在有效性上提升 20–25%。作者还将该工具应用于包含数百万行代码的工业级 C++ 代码库，并通过全面的人工验证确认了所生成规范的质量与实用价值。该工作表明，LLM 驱动的规范合成可有效支撑真实世界大规模底层 C++ 程序的自动化软件分析。
We present Fun2spec, the first industrial-strength tool guiding LLMs to synthesize C++ specifications in first-order logic with quantifiers. Fun2spec's very high accuracy (85%) employs an automated validation procedure with error-driven oracle feedback, and can even generate the strongest code contract 60% of the time. Our approach significantly outperforms previous methods, achieving 20–25% higher validity on standard benchmarks. We applied Fun2spec to very large scale industrial C++ codebases containing many millions of lines of code and performed comprehensive manual validation to confirm the quality and utility of the specification. Fun2spec stands as the first effective code contract synthesis tool for real-world large-scale low-level C++ programs, advancing the state-of-the-art in automated software analysis using LLMs.