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

AI 요약

Claude Code를 만든 Boris Cherny가 Opus가 TLA+로 코드의 경쟁 조건을 찾아냈다고 말한 뒤, 형식 검증이 에이전트 소프트웨어 개발의 문제를 해결하리라는 기대가 커졌습니다. TLA+를 오래 가르치고 사용해 온 글쓴이는 이 도구가 동시성 시스템 설계와 버그 탐색에 강하지만, 검증하려는 속성을 먼저 논리식으로 표현해야 한다는 한계를 강조합니다. 사람도 새도 알아보지 못하는 앱의 정확성을 형식 검증만으로 증명할 수는 없습니다.

TLA+가 검증하는 속성

TLA+에서 시스템 실행은 상태의 연속인 동작(behavior)으로 표현합니다. 상태마다 참·거짓을 판정하는 조건을 둘 수 있고, 시간 연산자를 붙여 여러 상태에 걸친 조건을 나타냅니다. []P는 현재부터 모든 미래 상태에서 P가 참이라는 뜻입니다. 예를 들어 모든 상태에서 초록불이 하나 이하라는 조건은 안전 속성(safety property)입니다. P'는 다음 상태에서 P가 참인지 나타내며, <>P는 현재나 미래 어느 상태에서든 P가 참인 경우를 뜻합니다.

이 연산자를 조합하면 생존 속성(liveness property)도 표현합니다. []<>P는 어느 상태에서 출발하든 이후 언젠가 P가 참이 되는 상태가 다시 나타난다는 뜻입니다. 새 리더 선출이 시작되면 결국 노드가 리더에 합의하는 상황을 나타낼 수 있습니다. <>[]P는 어느 시점부터 P가 계속 참임을 표현해 알고리즘이 올바른 결과로 끝나는 경우를 다룹니다. [](P => <>Q)는 P가 참인 모든 상태에서 이후 Q가 참이 되는 상태가 있음을 뜻하며, P ~> Q로 줄여 쓸 수 있습니다. 불변식(invariant), 동작 속성(action property), 생존 속성, 정제(refinement)가 TLA+에서 주로 확인하는 대상입니다.

표현하기 어려운 속성

속성을 논리식으로 정식화하지 못하면 TLA+뿐 아니라 어떤 형식 기법으로도 검증하기 어렵습니다. TLA+의 안전 속성은 개별 상태나 한 번의 상태 전이에 적용되므로, 여러 단계에 걸친 조건을 바로 표현하지 못합니다. 삭제한 뒤 실행 취소하면 원래 상태로 돌아오는지, 전원 버튼을 누른 뒤 열 단계 안에 컴퓨터가 켜지는지 같은 조건이 예입니다. 부동소수점 연산이나 실제 시간도 기본적으로 다루지 않으며, 논리적 시간에 초점을 맞춥니다.

더 큰 제약은 TLA+ 속성이 모든 동작을 대상으로 한다는 점입니다. 따라서 특정 속성을 만족하는 실행이 하나라도 존재하는지 묻는 도달 가능성(reachability)을 자연스럽게 표현하기 어렵습니다. 게임에서 승리할 수 있는지 증명하는 문제가 한 예입니다. 두 실행을 서로 비교해야 하는 하이퍼속성(hyperproperty)도 마찬가지입니다. 절전 모드가 일반 모드보다 항상 전력을 덜 쓰는지 확인하려면, 같은 입력을 받은 두 실행의 전력 사용량을 비교해야 합니다. 한 실행만으로는 반례를 구성할 수 없습니다. 하이퍼속성은 보안 속성과 백분위 응답 시간 같은 통계 속성을 포함합니다. 상태 공간 전체를 대상으로 경로가 하나뿐인지 묻는 메타속성도 기본 표현 범위에 들어오지 않습니다.

우회 기법과 비용

보조 변수(auxiliary variable)에 상태 변경 기록을 저장하면 여러 단계 조건을 불변식으로 바꿔 표현할 수 있습니다. 자기 합성(self-composition)은 실제 시스템의 실행 둘을 하나의 모델 실행에 담아 하이퍼속성을 다룹니다. TLC는 REACHABLE 키워드로 기초적인 도달 가능성을, TLCGet으로 일부 상태 공간 속성을 확인할 수 있습니다. 공정성(fairness)과 기계적 폐쇄성(machine closure)을 활용해 언제나 도달 가능함을 흉내 내는 방법도 있습니다.

하지만 이런 방법은 우회책입니다. 보조 변수는 정제 작업을 방해할 수 있고, 자기 합성은 상태 공간을 크게 늘립니다. 다른 TLA+ 기능과 조합하기도 쉽지 않으며, 모델이 실제 시스템과 동떨어져 보일 수 있습니다. CTL은 도달 가능성, PRISM은 확률 속성에 초점을 맞추지만, 각 도구는 TLA+가 잘 다루는 영역에서 다른 제약을 둡니다. 글쓴이는 불변식과 생존 속성만으로도 많은 버그를 찾을 수 있지만, TLA+가 표현조차 못 하는 속성이 상당하다고 정리합니다.

Lobsters 반응

• @ahelwer — 어떤 속성은 TLA+로 표현하기가 훨씬 수월합니다. 제가 쓴 도달 가능성 속성 글은 정말 난해했습니다. TLA+를 10년 넘게 써 왔고 핵심 도구 작업으로 돈을 받은 적도 있으며, 아마 전 세계에서 TLA+를 가장 잘 아는 사람 다섯에서 열 명 안에 들 텐데, 그 글을 쓰기 전까지 도달 가능성을 어떻게 표현하는지 이해하지 못했습니다. 그러니 기술적으로 표현할 수 있더라도 사용하기 불편한 경우가 있다는 말은 타당합니다. 이 불편함이 형식 자체의 한계인지, 형식을 확장해 개선할 수 있는지 궁금합니다. 확장하면 1950년대 Arthur Prior가 시간 논리를 만든 뒤 이어진 분기 시간 논리와 선형 시간 논리의 논쟁에 다시 빠지는 건지도 궁금합니다. 적어도 TLC는 기본 도달 가능성을 쉽게 확인하도록 확장할 수 있겠지만, 다른 속성과 조합하는 방식은 아닐 겁니다.
  • @hwayne — CTL*은 도달 가능성과 생존 속성을 모두 확인할 수 있다고 들었는데, CTL* 기반 도구는 본 적이 없습니다. 어떤 문제가 있는지 궁금합니다.
  • @ahelwer — CTL*에 분기 시간 논리와 선형 시간 논리를 어떻게든 함께 담는다는 점이 특이하다고 들었습니다. 그 이상은 모르지만, 전에 본 적 없는 2002년 논문 「분기 시간 대 선형 시간: 최후의 결전」은 찾아냈습니다.
• @Student — 정말 좋은 글입니다. 표현 가능한 속성이 무엇인지 간결하게 정리했습니다. 다른 형식 기법으로 표현할 수 있는 속성을 알려 주는 사전이 있으면 좋겠습니다. 바로 쓸 수 있는 검사기가 없더라도 무엇을 명세할지 생각하는 길잡이가 될 것 같습니다. 코드를 추론하고, 그런 속성을 검사하거나 반증할 테스트를 작성하는 데 도움이 되겠습니다.

원문: Buttondown / 번역·요약: Trawling