用AI自动生成代码规范并自动查错，发现249个深层漏洞
Specula: Scaling formal specifications for autonomous model checking of system code
- 用大模型自动生成TLA+规范，包含正确性断言和抽象实现模型
- 在48个开源系统中检测出249个漏洞，包括传统方法难发现的深层缺陷
- 全自动闭环优化，防止幻觉与奖励滥用，适合工业级系统验证
Specula是一个全自动的智能系统，可为大型复杂系统代码自动生成高质量的形式化规范，并用于高效模型检测与漏洞发现。该系统利用基于大语言模型的编码代理，自主构建TLA+规范，包括描述系统正确性性质的不变量以及以恰当抽象层次描述系统实现的形式化模型。Specula完全自动化，消除了传统人工驱动形式化方法在真实系统代码应用中的门槛。同时，通过自演化循环机制，Specula有效应对大模型技术常见的奖励劫持和幻觉问题，使代理能持续深化对代码及其行为的理解，迭代提升规范质量。我们已使用Specula检查了48个开源系统项目，共发现249个漏洞，其中许多是现有方法难以察觉的深层缺陷。Specula已被多家公司采用，代码维护于https://github.com/specula-org/Specula。
原文摘要 · Abstract (English)
Specula is a push-button agentic system that generates high-quality formal specifications for large, complex system code and uses the specifications for highly effective model checking and bug finding. Specula employs large language model (LLM) based coding agents to autonomously develop TLA+ specifications, including invariants that describe correctness properties of the target system and formal models that describe the system implementation with the right level of abstractions. Specula is fully autonomous and thus eliminates the barrier of applying formal methods to real-world system code (as in traditional human-centric approaches). Meanwhile, Specula addresses limitations of LLM-driven techniques like reward hacking and hallucinations through self-evolving loops that iteratively improve specification quality by enabling the agents to deepen their understanding of system code and its behaviors. We have used Specula to check 48 open-source system projects; Specula found 249 bugs including many deep bugs that are hard to find by existing approaches. Specula has been used by several companies and is maintained at https://github.com/specula-org/Specula.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。