Specula：系统代码自主模型检查的扩展形式规范

Specula 是一个按钮式代理系统，可为大型、复杂的系统代码生成高质量的正式规范，并使用这些规范进行高效的模型检查和错误查找。 Specula 采用基于 大语言模型 (LLM) 的 编码智能体 来自主开发 TLA+ 规范，包括描述目标系统正确性属性的不变量以及描述具有正确抽象级别的系统实现的形式模型。 Specula 是完全自主的，因此消除了将形式方法应用于现实世界系统代码的障碍（如传统的以人为中心的方法）。同时，Specula 通过自我进化循环解决了 LLM 驱动技术（如 奖励作弊 和幻觉）的局限性，通过使代理加深对系统代码及其行为的理解，迭代地提高规范质量。我们使用Specula检查了48个开源系统项目； Specula 发现了 249 个错误，其中包括许多现有方法难以发现的深层错误。 Specula 已被多家公司使用，并在 https://github.com/specula-org/Specula 进行维护。