TLA+가 검증할 수 없는 것들
원제: What TLA+ can and can't check
왜 중요한가
AI가 TLA+를 활용한다는 소식이 형식 검증 만능론으로 번지는 흐름 속에서, 도구의 실제 적용 범위를 냉정히 짚는 논의는 업계의 기대 조정에 직접적인 영향을 미친다.
Claude Code 발명자 Boris Cherny가 Opus를 이용해 TLA+로 레이스 컨디션을 찾아냈다고 밝힌 후, 형식 검증(formal verification)이 AI 에이전트 개발의 만능 해법이라는 주장이 확산됐다. TLA+ 장기 교육자인 Hillel Wayne은 2026년 9월 30일 뉴스레터를 통해 이 낙관론에 제동을 걸며 TLA+의 구조적 한계를 구체적으로 설명했다.
TLA+는 복잡한 동시성 시스템(concurrent systems)을 설계하고 버그를 사전에 잡아내는 데 강점을 지닌 형식 명세 언어다. 시스템을 '행동(behavior)'의 집합, 즉 상태의 시퀀스로 분해해 불변식(invariant), 안전 속성(safety property), 활성 속성(liveness property)을 수학적으로 검증한다. []P('항상 P'), <>P('언젠가 P'), P'('다음 상태의 P') 같은 시제 논리 연산자를 조합하면 '노드가 새 리더 선출 후 결국 합의에 이른다'거나 '알고리즘이 올바른 결과로 종료된다' 같은 속성을 표현할 수 있다.
문제는 검증할 속성이 사전에 명확히 정의돼 있어야 한다는 점이다. Wayne은 '올바른 설계가 자동으로 올바른 코드로 이어지지 않는다'는 이미 알려진 한계보다, 더 근본적인 한계를 지적한다. TLA+는 속성을 부울 식으로 표현하는데, 시스템이 무엇을 해야 하는지 언어로 정의하기 어렵거나 아예 불가능한 속성들이 존재한다. 성능 요구사항, 사용자 의도의 모호함, 비결정론적 환경에서의 기대치 같은 것들은 TLA+ 명세로 옮기는 것 자체가 난제다.
그는 AI 에이전트 소프트웨어 개발에서 형식 검증이 '모든 문제를 해결한다'는 식의 주장을 '말이 안 된다(nonsense)'고 직접 표현했다. TLA+가 강력한 도구임은 분명하지만, 검증 대상 속성을 정의하는 작업 자체가 여전히 사람의 몫이라는 것이 핵심 논지다.