Reasonable AI, TLA+ 사양을 Verus 증명으로 변환하는 파이프라인 공개

Reasonable AI가 TLA+ 사양을 Verus의 기계 검증 가능한 증명으로 변환하는 에이전틱 파이프라인을 개발했다. 이는 최근 Opus 5.5 같은 LLM을 활용한 에이전트 모델링 사례로 높아진 형식 방법론의 관심에 대응하기 위한 것이다.

사양에서 증명까지

**TLA+**는 시스템 동작을 기술하는 시제 논리 언어로 AWS, MongoDB, Datadog 등에서 널리 사용된다. 하지만 TLC 기반 모델 체크는 유한한 인스턴스만 검증할 수 있어 실제 구현 코드는 검증하지 못한다. Reasonable AI는 사양, 증명, 구현이 공존할 수 있는 Rust 기반 검증 도구 Verus를 활용해 코드와 모델의 일치성을 보장하는 정제 증명을 가능하게 했다.

에이전틱 검증 파이프라인

번역 및 증명 생성 과정을 자동화하기 위해 다음과 같은 시스템을 구축했다.

• 트랜스파일링: 알고리즘 기반 트랜스파일러로 TLA+ 사양을 Verus로 변환하며, 한 LLM이 번역하고 다른 LLM이 검토하는 에이전틱 방식과 비교했다.
• 증명자-검토자 루프: 한 에이전트가 증명을 생성하고 다른 에이전트가 이를 검토한다. 별도의 '게이트키퍼' 에이전트가 사양 변경 여부를 확인하고 assume(false) 같은 부정행위를 차단한다.
• 데이터셋 구축: 16,459개의 실제 TLA+ 사양/속성 쌍에서 시작해 3,000개 이상의 기계 검증 가능한 안전성 및 생존성 증명을 생성했다.
• 평가: 현재 폐쇄형 및 오픈 웨이트 프론티어 모델의 시제 증명 수행 능력을 테스트하기 위해 40개 태스크 평가 세트를 구성했다.

향후 방향

이 프로젝트는 불변식 추적이나 액션 분할 등 형식 검증의 반복적인 작업을 AI가 처리할 가능성을 보여준다. 향후에는 정제 증명(Rust 코드가 TLA+ 모델을 정제함을 증명), 프로그램 합성(코드와 증명을 함께 생성), 그리고 검증기를 목적 함수로 사용하는 프로토콜 탐색 등으로 확장할 계획이다.