LLM 시대에 다시 떠오르는 형식 검증 도구, TLA+ 입문

TLA+가 뭔가요, 그리고 왜 지금?

TLA+(티엘에이 플러스)라는 도구를 들어보셨나요? 들어보지 못했다면 자연스러운 일이에요. 분산 시스템을 설계하는 사람들 사이에서나 알려진 "형식 명세 언어(formal specification language)"거든요. Leslie Lamport라는 분산 컴퓨팅 분야의 거장이 만들었고, AWS 내부에서 DynamoDB나 S3 같은 핵심 시스템의 설계 검증에 쓰는 걸로 유명해요.

쉽게 말하면, 코드를 짜기 전에 "내 시스템이 어떤 상태에서 어떤 상태로 어떻게 옮겨가는지"를 수학에 가까운 언어로 적어두는 도구예요. 그렇게 적어두면 TLA+ 모델 체커가 가능한 모든 상태 조합을 자동으로 돌려보면서 "이런 순서로 일이 벌어지면 데드락이 생기네", "이 경합 조건에서 데이터가 깨지네" 같은 버그를 미리 잡아줘요. 테스트로는 절대 못 찾는, 백만 번에 한 번 발생하는 종류의 버그를 잡아내는 거죠.

문제는 진입 장벽이 너무 높았다는 거예요. 수학 기호 같은 문법, 직관적이지 않은 모듈 구조, 부족한 학습 자료. 그래서 "좋다고는 들었는데 나는 못 쓰겠다"는 사람들이 많았어요. 그런데 LLM이 등장하면서 이 그림이 바뀌고 있다는 게 이번 글의 핵심이에요.

LLM이 TLA+의 진입 장벽을 어떻게 낮추는가

원문 글쓴이는 TLA+의 가장 큰 허들이 "빈 페이지 문제"라고 말해요. 처음 명세를 적기 시작할 때 어디서부터 손을 대야 할지 모르겠는 그 막막함 말이에요. 그런데 LLM에게 "이런 시스템을 TLA+로 명세해줘"라고 시키면, 완벽하진 않아도 시작점이 되는 초안을 만들어줘요. 그 초안을 사람이 다듬는 흐름으로 가면, 백지에서 시작하는 것보다 훨씬 빠르게 진입할 수 있다는 거예요.

구체적인 예시도 흥미로워요. 글쓴이는 간단한 분산 카운터 시스템을 LLM에게 명세시켜본 다음, 모델 체커를 돌려서 LLM이 놓친 엣지 케이스를 발견하고, 그 결과를 다시 LLM에게 피드백해서 명세를 개선시키는 사이클을 보여줘요. 즉 LLM과 모델 체커가 서로의 약점을 보완하는 거예요. LLM은 "그럴듯한 명세"를 빠르게 만들지만 미묘한 경합 조건을 놓치고, 모델 체커는 그런 케이스를 정확히 잡아내지만 명세 자체는 사람이 써야 하니까요.

또 한 가지 인상 깊은 포인트는 "LLM에게 코드를 시키면 그럴듯한 잘못된 코드를 내놓을 위험이 크지만, TLA+ 명세를 시키면 모델 체커가 검증해주기 때문에 LLM의 환각(hallucination)을 시스템적으로 잡을 수 있다"는 주장이에요. 다시 말해 형식 검증은 LLM 시대에 오히려 더 가치 있어진다는 거죠.

비슷한 도구들과 비교

형식 검증 도구는 TLA+ 말고도 여럿 있어요. Alloy는 좀 더 객체 지향적이고 가벼운 분석에 적합하고, Coq나 Lean은 수학 정리 증명에 가까운 무거운 도구예요. P 언어는 마이크로소프트가 비동기 시스템 검증용으로 만든 거고, 최근에는 Rust 생태계의 Kani나 Verus 같은 도구도 등장했어요.

TLA+의 강점은 "동시성과 분산"이라는 좁고 깊은 영역에 특화돼 있다는 거예요. 그래서 합의 알고리즘(Raft, Paxos), 분산 트랜잭션, 캐시 일관성 같은 문제에 진가를 발휘해요. 단점은 추상화 수준이 너무 높아서, 실제 코드와 명세 사이를 사람이 손으로 이어줘야 한다는 점이에요. TLA+로 검증한 명세가 맞다고 해서 그걸 구현한 Go 코드도 맞다는 보장은 없거든요.

그래서 최근에는 "명세는 TLA+로, 구현은 Rust나 Go로, 둘 사이의 일관성을 LLM과 테스트로 메운다"는 접근이 조심스럽게 시도되고 있어요. 이번 글도 그 흐름의 일부라고 볼 수 있어요.

한국 개발자에게 어떻게 다가갈까

국내에서 TLA+를 실무에 쓰는 회사는 손에 꼽을 정도예요. 대부분의 서비스는 형식 검증까지 안 가도 충분히 동작하니까요. 하지만 결제, 정산, 재고, 메시징처럼 "한 번이라도 틀리면 큰일 나는" 도메인을 다루는 분들에게는 진지하게 고려할 가치가 있어요. 특히 마이크로서비스 간에 분산 트랜잭션을 처리해야 하거나, 큐와 워커 사이의 메시지 순서를 보장해야 하는 경우에 그래요.

예전엔 "TLA+ 한번 배워보자"고 마음먹어도 책 한 권을 떼는 데 몇 주가 걸렸어요. 이제는 Claude나 GPT에게 "이 시나리오를 TLA+로 적어줘"라고 시키면서 같이 공부하면, 진입 비용이 훨씬 줄어들어요. 한 달 정도만 투자해도 간단한 분산 시스템 검증은 충분히 시도해볼 수 있을 거예요.

또 시니어 엔지니어로 성장하려는 분들이라면 "내가 짠 시스템이 왜 맞는지"를 설명할 수 있는 능력이 점점 더 중요해질 거예요. 단순히 테스트가 통과한다고 맞다고 말하는 건 약한 논증이거든요. TLA+ 명세를 한 번이라도 써본 경험은 그런 사고력을 키우는 데 큰 도움이 됩니다.

마무리

LLM이 나오면서 "이제 형식 검증 같은 거 안 해도 되지 않냐"는 말도 나오지만, 글쓴이의 주장은 정반대예요. LLM이 만든 코드를 신뢰하려면 오히려 형식 검증이 더 필요해지고, LLM은 그 검증을 사람이 쓰기 쉽게 만들어주는 보조 도구가 된다는 거죠. 여러분은 LLM이 생성한 코드를 검토할 때, 어떤 방식으로 "이 코드가 맞다"는 확신을 얻고 계세요?