형식 검증의 새로운 시대, TLA+와 AI가 만나다

핵심 요약

• 보리스 체르니의 바이럴 트윗 이후 TLA+에 관심이 몰리고 있으며, 이 글은 TLA+의 실용성과 한계, 그리고 미래 방향을 설명한다.
• TLA+(Temporal Logic of Actions)는 시스템의 가능한 동작과 만족해야 할 성질을 기술하는 형식 언어로, 상태와 행동으로 이루어진 전이 시스템을 모델링한다.
• TLA+의 모델 체커인 TLC는 유한 모델의 모든 가능한 실행을 탐색해 안전성(bad thing이 일어나지 않음)과 생존성(good thing이 결국 일어남) 같은 시간적 성질을 검증한다.
• TLA+ 단독으로는 세 가지 한계가 있다: 유한 모델만 확인 가능하고, 사양과 구현의 간극을 자동으로 메워주지 않으며, 선형 시간 논리만 표현할 수 있다.
• Lean과 Verus 같은 현대 증명 시스템을 이용하면 더 강력한 검증이 가능하며, 특히 Verus는 Rust 구현과 사양을 같은 언어로 작성할 수 있어 사양-구현 간극을 줄일 수 있다.
• 형식 검증의 증명 작업은 대부분 반복적이고 자동화 가능한 패턴(불변식 추적, 행동 분류, 중간 보조정리 제공)으로 이루어져 있어 AI 에이전트의 자동화 대상이 된다.
• Reasonable 팀은 TLA+ 사양 16,459개로부터 3,000개 이상의 기계 검증된 Verus 증명을 생성하는 파이프라인을 구축했으며, 여기에는 LLM 기반 변역기, 증명-검수 루프, 반부정행위 체크가 포함되어 있다.
• 향후 방향은 세 가지다: TLA+ 모델이 Rust 구현을 따르는지 증명하는 정제 증명, 모델과 그에 맞는 구현을 함께 생성하는 프로그램 합성, 올바른 프로토콜을 자동으로 찾아내는 프로토콜 검색이다.