Specula: Scaling formal specifications for autonomous model checking of system code

📄 arXiv: 2607.25333v1 📥 PDF

作者: Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, Tianyin Xu

分类: cs.SE, cs.AI, cs.DC, cs.OS

发布日期: 2026-07-28

备注: 17 pages, 11 figures

🔗 代码/项目: GITHUB

💡 一句话要点

提出Specula以解决复杂系统代码的形式化规范生成问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化规范 模型检查 自动化测试 大型语言模型 软件工程 缺陷发现

📋 核心要点

  1. 现有方法在复杂系统代码的形式化规范生成上存在效率低下和准确性不足的问题。
  2. Specula通过自动生成TLA+规范，利用大型语言模型的编码能力，提升了形式化方法的应用效率。
  3. 在48个开源项目中，Specula发现了249个缺陷，显著提高了缺陷检测的深度和准确性。

📝 摘要（中文）

Specula是一个自动化的代理系统，能够为大型复杂系统代码生成高质量的形式化规范，并利用这些规范进行高效的模型检查和缺陷发现。Specula采用基于大型语言模型的编码代理，自动开发TLA+规范，包括描述目标系统正确性属性的不变式和以适当抽象级别描述系统实现的形式模型。Specula完全自主，消除了将形式方法应用于现实系统代码的障碍，同时通过自我演化循环解决了奖励黑客和幻觉等LLM驱动技术的局限性。我们在48个开源系统项目中使用Specula，发现了249个缺陷，其中包括许多现有方法难以发现的深层缺陷。

🔬 方法详解

问题定义：论文旨在解决复杂系统代码的形式化规范生成问题，现有方法往往依赖人工，效率低且容易出错。

核心思路：Specula通过自动化生成TLA+规范，利用大型语言模型的能力，消除了人力干预的需求，从而提高了形式化方法的适用性和效率。

技术框架：Specula的整体架构包括编码代理、规范生成模块和自我演化循环。编码代理负责解析系统代码并生成相应的TLA+规范，规范生成模块则确保生成的规范符合系统的正确性要求。

关键创新：Specula的主要创新在于其完全自主的生成过程和自我演化机制，能够在不断迭代中提升规范质量，克服了传统LLM方法的局限性。

关键设计：在设计中，Specula采用了自我演化循环，通过反馈机制不断优化生成的规范，确保其准确性和有效性，同时避免了奖励黑客和幻觉等问题。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

在实验中，Specula对48个开源系统项目进行了检查，发现了249个缺陷，其中包括许多深层缺陷，这些缺陷是现有方法难以检测到的，显示了Specula在缺陷发现方面的显著优势。

🎯 应用场景

Specula的研究成果在软件工程、系统验证和自动化测试等领域具有广泛的应用潜力。其自动生成的形式化规范可以帮助开发者更高效地进行系统验证，提升软件的可靠性和安全性。未来，Specula有望在更多复杂系统的开发和维护中发挥重要作用。

📄 摘要（原文）

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.