TLA+ 교육자 힐렐 웨인, "LLM이 형식 검증으로 에이전트 개발을 해결한다"는 낙관론에 제동

Claude Code를 만든 보리스 체르니가 Opus 5.5로 Claude Agent SDK를 Lean으로 형식 검증해 버그와 경쟁 조건을 고친 PR 16개를 올렸다고 밝힘. 데이터 흐름, 동시성, 상태 관리 문제에는 TLA+도 병행한다고 함.
TLA+ 교육자이자 전도사인 힐렐 웨인은 형식 기법이 에이전트 소프트웨어 개발 문제를 완전히 해결한다는 기대는 헛되다고 반박함. 이번 글은 TLA+의 보장 한계가 아니라 표현조차 못 하는 속성에 초점을 맞춤.
TLA+는 시스템을 상태 열인 behavior로 나누고, 각 상태의 불리언 식에 always, next, eventually 세 시간 논리 연산자를 붙여 검증함. 신호등 예로 보면 always(at_most_one_green), light="green" && light'="red", eventually(light4="yellow") 같은 식을 씀.
설계가 맞아도 코드가 맞다는 보장은 없다는 한계는 다른 글에서 이미 다뤘고, 이 글은 검증할 속성이 먼저 표현 가능해야 검증도 가능하다는 점을 짚음.

Hacker News 의견들

좋은 글임. 사람들은 '테스트 쓰면 되지' 아니면 요즘엔 '형식 검증 쓰면 되지' 하면서 구현은 다 LLM에 맡기면 된다고 생각하는데, 확률로 추측하는 기계가 그걸 해결해주진 않음. 결국 자기가 만드는 걸 이해해야 함.

근데 이건 프로그래밍 언어 문제이기도 한 듯. 대부분 언어가 부분 그래프만 표현할 수 있어서 검증이 기술적으로 어려워짐. 닫힌 그래프 의미론만 노출하는 언어라면 모델과 구현 사이 간극을 좁히는 데 도움이 될지도. 절대적이진 않아도.

이 댓글 보고 Quint 알게 됐음. TLA의 temporal logic of actions 기반이고 JavaScript에서 돌아가는 실행 가능한 명세 언어인데 툴링이 좋음. TLA+에 관심 있으면 한번 봐봐라.

관련 글로 'The internet discovers TLA+. Now what?'도 있음. HN에서 한참 돌았던 그 글.

형식 기법이 못 잡는 것도 분명히 있음. 부동소수점 비결합성이나 사이드 채널 같은 건 애초에 기대하면 안 되는 항목이고, 검증 안 된 하드웨어나 펌웨어 쪽 사이드 채널은 우회만 가능함. 다른 레이어 얘기긴 한데.