Specula: 시스템 코드의 자율적 모델 검증을 위한 형식 명세 확장

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

Specula는 대규모 복잡한 시스템 코드를 위한 고품질 형식 명세를 자동으로 생성하고, 이를 활용하여 효과적인 모델 검증 및 오류 탐지를 수행하는 에이전트 기반 시스템입니다. Specula는 대규모 언어 모델(LLM) 기반의 코딩 에이전트를 사용하여 대상 시스템의 정확성 속성을 설명하는 불변 조건과 시스템 구현을 적절한 수준으로 추상화하여 나타내는 형식 모델을 포함한 TLA+ 명세를 자율적으로 개발합니다. Specula는 완전 자동화되어 있어, 기존의 인간 중심 접근 방식에서 발생하는 형식 방법론 적용의 장벽을 제거합니다. 또한, Specula는 자체 진화 루프를 통해 에이전트가 시스템 코드 및 동작에 대한 이해도를 높여 규격 품질을 반복적으로 개선함으로써 LLM 기반 기술의 한계점인 보상 해킹 및 환각 현상을 해결합니다. 저희는 Specula를 사용하여 48개의 오픈 소스 시스템 프로젝트를 검증했으며, 기존 방식으로는 발견하기 어려운 많은 심층 오류를 포함하여 총 249개의 오류를 발견했습니다. Specula는 여러 기업에서 사용되고 있으며, GitHub 저장소(https://github.com/specula-org/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.