"AI가 TLA+로 버그 다 잡는다고?" 정형 검증 전문가가 찬물 끼얹은 이유

요약 최근 앤트로픽 클로드 코드(Claude Code) 개발자인 보리스 체르니(Boris Cherny)가 '클로드 오퍼스(Opus) 모델이 TLA+를 활용해 코드 내 레이스 컨디션(경쟁 상태)을 찾아냈다'고 밝히면서 실리콘밸리와 해외 개발자 커뮤니티에서 정형 검증(Formal Verification) 열풍이 불기 시작했습니다. AI가 복잡한 시스템을 TLA+로 완벽히 검증해 소프트웨어 개발의 고질적인 버그들을 모두 해결해 줄 것이라는 낙관론이 쏟아져 나온 것입니다. 하지만 오랜 기간 TLA+ 교육자이자 옹호자로 활동해 온 힐렐 웨인(Hillel Wayne)은 이러한 'AI 구원론'에 대해 경계하며 냉정한 현실을 짚었습니다. 올바른 설계가 저절로 버그 없는 코드로 이어지지 않는다는 기존의 한계 외에도, TLA+ 자체가 애초에 표현조차 할 수 없는 속성들이 많다는 지적입니다. TLA+를 쓰려면 검증하고자 하는 대상의 속성을 명확한 논리식으로 기술해야 하는데, 현실 세계의 모호한 개념(예: 앱이 '새'를 올바르게 인식하는지 여부)은 수식화 자체가 불가능해 검증 도구가 개입할 여지가 없습니다. 또한 TLA+의 세부적인 표현 한계도 존재합니다. 안전성 속성은 단일 상태(불변성)나 직후 상태(액션 속성) 수준에서만 작동하기 때문에, '삭제 후 실행 취소를 누르면 원래 상태로 돌아온다'거나 '전원을 켠 뒤 10단계 안에 켜진다'처럼 2단계 이상의 과정을 묶은 명제는 기본적으로 표현하기 어렵습니다. 실수 연산(부동소수점)이나 현실의 물리적 시간(Real time) 역시 다룰 수 없습니다. 무엇보다 TLA+는 모든 개별 행동(Behavior)에서 항상 참이어야 하는 전칭 속성만을 기본 전제로 하기 때문에, '게임이 승리 가능한 상태에 도달할 수 있는가'와 같은 도달 가능성(Reachability)이나 '어떤 행동이 존재한다'는 식의 존재 양화 명제는 다루기 까다롭습니다. 결국 TLA+가 강력한 도구인 것은 분명하지만, AI가 가져다 쓸 때 모든 개발 문제를 단번에 해결해 주는 만능 치트키는 아니라는 설명입니다.