지난주 Claude Code를 만든 Boris Cherny가 Opus 모델이 TLA+를 활용해 코드의 경쟁 조건(race condition)을 찾아냈다고 언급하면서, 형식 검증(formal verification)이 다시 개발자 커뮤니티의 화제로 떠올랐다. AI가 스스로 짠 코드를 형식 기법으로 검증하면 '에이전트 기반 소프트웨어 개발'의 신뢰성 문제가 단번에 해결될 것이라는 기대도 함께 번졌다. 오랜 기간 TLA+를 가르치고 옹호해 온 Hillel Wayne은 이 흐름이 반가우면서도 과열된 낙관론에는 선을 긋는다. TLA+가 복잡한 동시성 시스템을 설계하고 버그를 걸러내는 데 뛰어난 도구인 것은 분명하지만, 모든 문제를 해결해 준다는 서사는 과장이라는 것이다.
그가 주목하는 한계는 흔히 지적되는 '올바른 설계가 올바른 코드로 자동 번역되지 않는다'는 지점이 아니다. 더 근본적인 문제는 검증하려면 먼저 '검증할 속성(property)'을 논리식으로 표현할 수 있어야 한다는 데 있다. TLA+는 시스템을 여러 동작(behavior), 즉 상태의 연속으로 나누어 본다. 각 상태에서 불리언 식을 평가하고, '항상(always, []]'·'언젠가(eventually, )' 같은 시간 논리 연산자로 이를 조합한다. 이렇게 만든 속성 중 가장 기본적인 것이 모든 상태에서 참이어야 하는 불변식(invariant)과, '나쁜 일은 결코 일어나지 않는다'는 안전성(safety), '좋은 일은 언젠가 반드시 일어난다'는 생존성(liveness)이다. 실무에서 검증하는 대부분이 이 범주에 들어간다.
애초에 표현할 수 없는 속성들
문제는 이 틀 바깥에 있는 속성들이다. 첫째, 논리식으로 형식화할 수 없는 성질은 TLA+뿐 아니라 어떤 형식 기법으로도 다룰 수 없다. '새'라는 인간의 개념을 수식으로 정의할 수 없다면, 어떤 앱이 새를 제대로 인식하는지도 증명할 수 없다. 우리가 정작 중요하게 여기는 많은 속성이 여기에 속한다. 둘째, 지나치게 구체적인 성질이다. TLA+의 안전성은 개별 상태나 한 번의 단계(step) 단위로만 정의되기 때문에, '삭제 후 실행 취소를 하면 원래 상태로 돌아온다'처럼 두 단계 이상에 걸친 속성이나 부동소수점 연산, 실제 물리적 시간에 대한 성질은 기본적으로 표현하기 어렵다. TLA+가 다루는 것은 논리적 시간이지 실시간이 아니다.
저자가 가장 흥미롭게 꼽는 한계는 TLA+의 속성이 암묵적으로 '모든 동작에 대해' 정량화된다는 점이다. '[]P가 성립한다'는 말은 사실 '모든 동작 각각에 대해 그 성질이 참'이라는 뜻이다. 따라서 '어떤 동작에서는 P가 참이다'와 같은 존재 명제는 자연스럽게 표현되지 않는다. 게임이 공략 가능한지(winnable)를 증명하는 것과 같은 도달 가능성(reachability) 속성이 대표적으로 빠진다. 특정 상태가 실제로 도달 가능하다는 사실조차 기본 틀에서는 말하기 어렵다.
하이퍼속성과 보안·통계 지표
더 까다로운 것은 여러 동작을 한꺼번에 비교해야 하는 하이퍼속성(hyperproperty)이다. 예컨대 '절전 모드가 일반 모드보다 전력을 더 쓰지 않는다'를 반박하려면, 초기 조건만 다른 두 동작을 나란히 놓고 비교해야 한다. 단일 동작 하나만 보아서는 판정할 수 없으므로 TLA+가 자연스럽게 다룰 수 없다. 저자는 이 부류가 niche해 보이지만 실제로는 상당수의 보안 속성과 '95퍼센타일 응답시간이 5ms 이하'와 같은 모든 통계적 속성을 포괄한다고 지적한다. 성능과 보안이라는, 실무에서 결코 사소하지 않은 영역이 여기에 걸린다.
우회로가 없는 것은 아니다. 상태 변화 이력을 보조 변수(auxiliary variable)에 저장해 다단계 속성을 불변식처럼 흉내 내거나, 명세를 자기 자신과 합성(self-composition)해 하이퍼속성 일부를 다룰 수 있다. 주력 모델 검사기인 TLC는 새로 도입된 REACHABLE 키워드로 기초적인 도달 가능성을, TLCGet으로 일부 상태공간 속성을 확인한다. 그러나 저자는 이들이 어디까지나 '해킹'에 가깝다고 분명히 한다. 보조 변수는 정제(refinement) 검증을 망가뜨리고, 자기 합성은 상태공간을 지수적으로 폭증시킨다. 영리한 기교가 필요한 데다 다른 기능과 잘 조합되지 않고, 무엇보다 명세가 실제 시스템과 동떨어진 지저분한 모양이 되어 버린다. CTL이나 확률 검증 도구 PRISM처럼 초점이 다른 도구로 갈아탈 수도 있지만, 그 경우 TLA+가 잘하던 것을 포기해야 하는 맞교환이 생긴다.
한국 개발 현장에서 LLM이 생성한 동시성 코드를 TLA+로 검증하려는 시도가 늘어난다면, 이 구분선을 아는 것이 곧 기대치 관리다. 불변식과 생존성이라는 '낮게 달린 과실'은 TLA+로 효율적으로 딸 수 있고 그것만으로도 가치가 크다. 하지만 성능 분포, 에너지 효율, 상당수 보안 요건, 도달 가능성처럼 실무가 실제로 신경 쓰는 속성들은 애초에 표현조차 되지 않거나 값비싼 우회를 요구한다. 결국 TLA+는 설계 단계에서 특정 종류의 버그를 걸러 주는 강력한 보조 수단이지, AI가 짠 코드의 정당성을 포괄적으로 보증하는 만능 안전망이 아니다. 도구가 무엇을 검증하는지보다, 무엇을 아예 말할 수 없는지를 함께 이해할 때 비로소 형식 기법에 대한 기대가 현실에 발을 딛는다.