发表机构
Nanjing University; University of Illinois Urbana-Champaign; Microsoft Research Asia; University of British Columbia（南京大学; 伊利诺伊大学厄巴纳-香槟分校; 微软亚洲研究院; 不列颠哥伦比亚大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
Specula利用大语言模型编码代理为系统代码生成形式规范，通过自我进化循环解决LLM技术局限，实现自主模型检查，应用于48个开源项目发现众多错误，消除形式方法应用障碍，助力系统代码验证。
AI 中文摘要
Specula是一个一键式智能系统，为大型复杂系统代码生成高质量形式规范，并用于高效的模型检查和错误查找。它利用基于大语言模型的编码代理自主开发TLA+规范，包括描述目标系统正确性属性的不变式和以适当抽象级别描述系统实现的形式模型。Specula完全自主，消除了将形式方法应用于实际系统代码的障碍。同时，通过自我进化循环解决了LLM驱动技术的局限性，迭代提高规范质量。使用Specula检查了48个开源系统项目，发现249个错误，包括许多现有方法难以发现的深层错误。已有多家公司使用Specula，可通过此https URL维护。
英文摘要
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.
Comments17 pages, 11 figures
