TLA+가 검증할 수 있는 것과 없는 것

TLA+ 는 복잡한 동시성 시스템의 불변식과 활성 속성을 검증하는 데 유용하지만, 에이전트 기반 소프트웨어 개발의 모든 문제를 해결하지는 못함 검증하려면 원하는 속성을 논리식으로 표현할 수 있어야 하며, 올바른 설계가 자동으로 올바른 코드로 이어지는 것도 아님 TLA+의 속성은 모든 개별 동작 경로에서 성립해야 하므로, 특정 상태에 도달할 수 있는 경로가 존재하는지나 여러 경로 사이의 관계를 자연스럽게 표현하기 어려움 보조 변수와 자기 합성으로 일부 표현 한계를 우회할 수 있고 TLC도 일부 도달 가능성 검사를 지원하지만, 정제 관계 훼손이나 상태 공간 급증 같은 대가가 따름 바이브 코딩으로 만든 코드를 TLA+로 검증할 가능성과 함정이 모두 존재하며, CTL과 PRISM 같은 다른 도구도 각자의 강점과 한계가 있어 모든 속성을 다루지는 못함 형식 검증에 대한 기대와 전제 Claude Code를 만든 Boris Cherny가 Opus로 TLA+를 사용해 코드의 경쟁 상태를 찾았다고 밝힌 뒤, 형식 검증에 대한 관심이 커짐 TLA+ 는 동시성 시스템의 버그를 찾는 명세 언어이며, 이름은 “Temporal Logic of Actions”에서 유래함 이름에 대한 해설과 기초 설명을 참고할 수 있음 복잡한 동시성 시스템을 설계하고 검증하는 데 강점이 있지만, 형식 기법이 에이전트 기반 개발 문제를 완전히 해결한다는 기대는 과도함 올바른 설계가 자동으로 올바른 코드로 이어지지는 않음 그보다 앞선 제약으로, 검증하고 싶은 속성 자체를 명세 언어로 표현할 수 있어야 함 상태, 동작 경로와 시간 논리 TLA+는 시스템을 동작 경로(behavior)의 집합으로 다루며, 각 경로는 “신호등이 초록색, 노란색, 빨간색으로 바뀜” 같은 상태의 연속임 각 상태에서 “4번 신호등이 초록색임”, “모든 신호등이 빨간색임” 같은 불리언 식을 작성할 수 있음 다음 연산자로 시간에 따른 조건을 표현함 []P: 현재와 모든 미래 상태에서 P가 참임을 뜻함. [](at_most_one_green)은 앞으로 모든 상태에서 초록불이 최대 하나임을 나타냄 P': 다음 상태의 P를 나타냄. light="green" && light'="red"는 초록불에서 빨간불로의 전환을 나타냄 <>P: 현재 또는 적어도 하나의 미래 상태에서 P가 참임을 뜻함. <>(light4 = "yellow")는 4번 신호등이 현재 노란색이거나...