Can LLMs model real-world systems in TLA+?

TL;DR Highlight

LLM이 TLA+ 명세를 작성할 때 문법은 잘 통과하지만 실제 시스템과의 동작 일치도(conformance)는 46% 수준에 그친다는 걸 체계적으로 검증한 벤치마크 연구로, AI 기반 형식 검증의 현실적 한계를 보여준다.

Who Should Read

분산 시스템이나 동시성 코드를 설계/검증하는 개발자, 또는 LLM을 활용해 TLA+ 같은 형식 명세(formal specification) 작성을 자동화하려는 엔지니어.

Core Mechanics

이 연구를 시작한 계기는 Claude에게 Etcd의 Raft 구현에 대한 TLA+ 명세를 작성해달라고 했더니, Raft 논문 부록에 있는 명세를 그대로 가져다 냈기 때문이다. 문법도 맞고 모델 체커도 통과했지만, Etcd 실제 구현과는 무관한 명세였다.
이를 구별하기 위해 SysMoBench라는 자동 벤치마크를 만들었다. 동시성 동기화 및 분산 프로토콜을 포함한 11개 실제 시스템(ZooKeeper, etcd 등)을 대상으로, LLM이 생성한 TLA+ 명세를 4단계로 자동 평가한다.
4단계 평가는 순서대로 syntax(컴파일 가능 여부) → runtime(TLC 모델 체커 실행 오류 없는지) → conformance(실제 코드 실행 트레이스와 명세가 일치하는지) → invariant(안전성·활성 속성 만족 여부)로 구성된다.
Claude, GPT, Gemini, DeepSeek, Kimi, Qwen 등 주요 LLM을 평가한 결과, syntax 단계는 거의 완벽에 가깝게 통과하지만, conformance 평균은 46%, invariant 평균은 41%에 불과했다. 명세가 예쁘게 생겼다고 올바른 건 아니라는 걸 수치로 보여준다.
LLM 명세의 실패 패턴은 두 가지로 반복된다. 하나는 실제 시스템이 절대 도달할 수 없는 상태를 명세가 허용하는 것, 다른 하나는 실제 시스템이 반드시 도달하는 상태에 명세가 도달하지 못하는 것이다.
구체적 예시로, ZooKeeper Fast Leader Election(FLE) 명세에서 Claude Sonnet은 각 서버의 recvset(투표 수신 맵)을 map이 아닌 set union으로 구현했다. 실제 ZooKeeper는 같은 피어가 새 라운드에서 투표하면 이전 투표를 덮어쓰는데, LLM은 형식검증 교과서의 '모든 투표를 증거로 누적' 패턴을 따라서 두 투표를 모두 유지했다.
이런 오류가 발생하는 근본 원인은 LLM이 실제 구현 코드의 세부 동작을 추상화하는 게 아니라, 인터넷에 공개된 참고 논문이나 교과서 공식화 패턴을 재현하기 때문이다. LLM은 훈련 데이터에서 본 TLA+ 예제를 '기억'할 뿐이다.
SysMoBench는 단일 점수가 아닌 action별, invariant별로 세분화된 진단 결과를 제공한다. 어느 액션에서 실제 구현과 어긋나는지 정확히 찾아낼 수 있어서 단순 합격/불합격보다 훨씬 유용하다.

Evidence

실제 TLA+ 작성 경험자는 'LLM이 safety 속성은 어느 정도 도움이 되지만, liveness(활성) 속성을 올바르게 잡아내는 건 훨씬 어렵다'고 지적했다. 또한 LLM이 만든 모델에서 상태 공간 폭발(state space explosion)이 자주 발생하는데, 간단한 모델은 유도해주면 수정 가능하다는 경험도 공유됐다.
람포트(Lamport)의 '쓰지 않고 생각하는 건 생각하는 척일 뿐'이라는 말을 인용하며, 첫 초안은 반드시 직접 손으로 작성하고 전체 구조가 잡힌 후에 LLM을 추가 탐색 도구로 활용한다는 워크플로우를 소개한 댓글이 공감을 받았다.
TLA+와 별개로 Verus(구현 코드와 검증을 동시에 작성하는 Rust 기반 도구)를 옹호하는 의견이 있었다. 구현과 모델이 분리된 TLA+ 방식은 양쪽이 엇갈릴 위험이 있는데, Verus처럼 구현-검증을 결합하면 이 문제를 원천 차단한다는 주장이었다.
'LLM이 설계(TLA+)도 만들고 그 설계를 만족하는 코드도 쓴다면, 인간의 의도(intent)는 어디에 있는가? 인간이 원하는 걸 명시하지 않은 채 LLM이 검증까지 하면 무엇을 증명한 것인가?'라는 근본적 질문이 제기됐다.
'이름(Raft, Etcd 등)을 난독화한 소스코드만 주고 TLA+ 명세를 만들어달라면 어떤 결과가 나오나?'라는 질문이 댓글에 등장했는데, 이는 LLM이 이름 기반으로 학습 데이터를 재활용하는지 여부를 확인하는 흥미로운 실험 방향으로 주목받았다.
TLAiBench(https://github.com/tlaplus/TLAiBench)라는 별도 벤치마크도 소개됐다. 논리 퍼즐과 실세계 시나리오를 포함한 TLA+ 평가 데이터셋으로, SysMoBench와 유사한 방향의 커뮤니티 프로젝트다.
벤치마크 테스트 케이스 자체가 이미 LLM 훈련 데이터에 포함되어 있을 가능성을 지적한 댓글도 있었다. 완전히 새로운 복잡한 시스템 명세 설계에서 LLM이 어떤 성능을 보이는지가 진짜 핵심이라는 의견이었다.

How to Apply

LLM으로 TLA+ 명세를 생성한 후 '잘 컴파일되고 TLC가 통과하니 됐다'고 안심하고 싶을 때, SysMoBench의 conformance 단계처럼 실제 코드 실행 트레이스를 수집해 명세와 대조하는 검증 단계를 반드시 추가해야 한다. 문법 통과가 정확성을 보장하지 않는다.
LLM에게 Raft, Paxos 같은 유명 프로토콜의 구현체(예: etcd, ZooKeeper)에 대한 TLA+ 명세를 요청할 때는 시스템 이름을 난독화하거나 소스코드를 직접 붙여넣는 방식으로 제공해서, LLM이 논문 암기가 아닌 실제 코드 추상화를 하도록 유도하는 게 좋다.
구현과 검증 코드가 분리되면 양쪽이 엇갈릴 위험이 걱정된다면, Verus(https://github.com/verus-lang/verus) 같이 Rust 코드 안에서 직접 증명을 작성하는 도구를 검토할 수 있다. 이 방식은 모델-구현 불일치 문제를 구조적으로 차단한다.
TLA+ 명세 작성 워크플로우에서 LLM을 활용하려면, 첫 초안(특히 상태 변수 정의, 액션 분해 방식)은 직접 손으로 작성해서 시스템의 실제 데이터 구조를 반영하고, 그 이후 TLC 디버깅이나 invariant 탐색 단계에서 LLM을 보조 도구로 사용하는 방식이 더 안전하다.

Terminology

TLA+분산 시스템이나 동시성 알고리즘의 동작을 수학적으로 정확하게 기술하는 명세 언어. 레슬리 람포트(Lamport)가 만들었고, AWS나 Microsoft에서 실제 시스템 설계 검증에 사용한다.

TLCTLA+ 명세를 실행해서 가능한 모든 상태를 탐색하고 안전성/활성 속성 위반 여부를 검사하는 모델 체커(Model Checker). 자동화된 버그 탐지 도구라고 볼 수 있다.

conformanceTLA+ 명세와 실제 코드 구현이 얼마나 일치하는지 측정하는 것. 명세가 허용하는 상태 전이와 실제 프로그램 실행 트레이스를 비교해서 검사한다.

liveness property시스템이 '결국에는 좋은 일이 일어난다'는 속성. 예를 들어 '요청은 언젠가 반드시 처리된다'. 안전성(safety, '나쁜 일이 절대 일어나지 않는다')보다 검증하기 어렵다.

state space explosion모델 체커가 가능한 모든 시스템 상태를 탐색할 때, 상태 수가 기하급수적으로 늘어나 메모리나 시간이 부족해지는 현상. 명세가 너무 세밀하거나 변수가 많을 때 발생한다.

trace validation실제 코드를 실행해서 수집한 로그(트레이스)와 TLA+ 명세를 비교해 일치 여부를 확인하는 기법. 명세가 현실과 동떨어져 있지 않은지 확인하는 가장 실용적인 방법이다.