LLM이 형식 명세를 쉽게 써 주더라도, 초보자가 만든 명세는 컴파일조차 안 되거나 자명한 성질만 검증해 실제로는 아무것도 검증하지 못하는 경우가 많다. 미묘한 불변식, 라이브니스, 액션 성질처럼 형식 방법의 핵심 가치를 담은 명세를 LLM이 얼마나 잘 도울 수 있는지에 대한 한계와 가능성을 살펴본다.
InfoQ London에서 발표합니다. 대신 아래에 책 증정 이벤트가 있어요!
약 1년 전 AI is a gamechanger for TLA+ users를 썼는데, 거기서는 AI가 “명세(specification) 전투력 증폭기(force multiplier)”라고 주장했다. 그 글은 TLA+ 전문가가 이런 도구를 쓰는 관점에서 쓴 것이었다. 이제는 Github의 TLA+ 명세 중 4%에 어딘가 “Claude”라는 단어가 들어 있다. 이건 내게 흥미로운데, 형식 방법에 대한 관심은 원래 있었지만 사람들이 그걸 할 역량이 부족했을 뿐이라는 신호처럼 보이기 때문이다.
또 하나 흥미로운 점은, 초보자가 AI를 써서 형식 명세를 쓰면 무슨 일이 벌어지는지 감이 온다는 것이다. 결론부터 말하면 좋지 않다.
사례 연구로는 이 프로젝트를 보겠다. 대충 TLA+와 Alloy 명세를 ‘감’으로 찍어낸(vibed out) 정도는 되는 것 같다.
Alloy 명세부터 보자. 전체는 다음과 같다:
module ThreatIntelMesh
sig Node {}
one sig LocalNode extends Node {}
sig Snapshot {
owner: one Node,
signed: one Bool,
signatures: set Signature
}
sig Signature {}
sig Policy {
allowUnsignedImport: one Bool
}
pred canImport[p: Policy, s: Snapshot] {
(p.allowUnsignedImport = True) or (s.signed = True)
}
assert UnsignedImportMustBeDenied {
all p: Policy, s: Snapshot |
p.allowUnsignedImport = False and s.signed = False implies not canImport[p, s]
}
assert SignedImportMayBeAccepted {
all p: Policy, s: Snapshot |
s.signed = True implies canImport[p, s]
}
check UnsignedImportMustBeDenied for 5
check SignedImportMayBeAccepted for 5
여기서 몇 가지를 짚고 넘어가자. 첫째, 이건 실제로 컴파일이 안 된다. Boolean 표준 모듈을 쓰고 있으니 동작하려면 open util/boolean이 필요하다. 둘째, 여기서 Boolean을 쓰는 건 접근 자체가 잘못이다. 원래는 서브타이핑을 써야 한다.
sig Snapshot {
owner: one Node,
- signed: one Bool,
signatures: set Signature
}
+ sig SignedSnapshot in Snapshot {}
pred canImport[p: Policy, s: Snapshot] {
- s.signed = True
+ s in SignedSnapshot
}
즉, 이 사람이 실제로 이 명세를 돌려보지 않았다는 걸 알 수 있다. 이 문제는 TLA+에서는 어느 정도 덜 심각한데, 에이전트가 모델 체크를 돌릴 수 있게 해주는 공식 MCP 서버가 있기 때문이다. 그럼에도 나는 Reals를 쓰거나 NULL이 내장이라고 가정(사실은 사용자가 정의한 상수인데)하는 등, 모델 체크가 안 될 것 같은 명세를 정기적으로 본다.
하지만 더 큰 문제는 UnsignedImportMustBeDenied와 SignedImportMayBeAccepted가 _실제로는 아무것도 하지 않는다_는 점이다. canImport는 P || Q로 정의돼 있다. UnsignedImportMustBeDenied는 !P && !Q => !canImport를 검사한다. SignedImportMayBeAccepted는 P => canImport를 검사한다. 이건 항진식(tautology)이라서 언제나 참이다! 뭔가를 한다면, 기껏해야 canImport를 올바르게 정의했는지(정확히는, 그렇게 정의해두고 그 정의를 다시 확인하는지)만 확인할 뿐이다.
같은 일이 TLA+ 명세에서도 벌어진다:
GadgetPayload ==
/\ gadgetDetected' = TRUE
/\ depth' \in 0..(MaxDepth + 5)
/\ UNCHANGED allowlistedFormat
/\ decision' = "block"
NoExploitAllowed == gadgetDetected => decision = "block"
AI는 “자명한 성질(obvious properties)”만 쓰고 있다. 이런 성질은 “가드 절을 빠뜨렸다”거나 “변수를 업데이트하는 걸 잊었다” 같은 이유로 깨진다. 하지만 동시성, 비결정성, 혹은 여러 단계 떨어진 곳에서 분리되어 나타나는 잘못된 동작 때문에 깨지는 “미묘한(subtle)” 성질을 쓰는 데에는 별로 강해 보이지 않는다. 자명한 성질은 시스템을 이해하고, 시스템이 기대대로 동작하는지 확인하는 데는 유용하다. 하지만 형식 방법을 쓰는 진짜 가치는 미묘한 성질에서 나온다.
(이건 Strong and Weak Properties와도 연결된다. LLM이 만든 성질은 약하고, 의도된 성질은 강해야 한다.)
이건 AI가 쓴 거의 모든 FM 명세에서 보는 문제다. LLM은 명세의 핵심 기능 중 하나를 수행하지 못하고 있다. Prediction: AI will make formal verification go mainstream나 When AI Writes the World's Software, Who Verifies It? 같은 글은 LLM이 형식 방법을 대중화할 거라고 주장하지만, 명세를 쉽게 쓸 수 있다는 것만으로는(그 명세가 실제로 아무것도 검증하지 못한다면) 정확성에 도움이 되지 않는다.
나는 LLM과 TLA+에 관심을 갖게 된 계기가 The Coming AI Revolution in Distributed Systems였다. 그 글의 저자는 나중에 훨씬 더 복잡한 성질을 가진 명세를 ‘vibecoding’했다:
NoStaleStrictRead ==
\A i \in 1..Len(eventLog) :
LET ev == eventLog[i] IN
ev.type = "read" =>
LET c == ev.chunk IN
LET v == ev.version IN
/\ \A j \in 1..i :
LET evC == eventLog[j] IN
evC.type = "commit" /\ evC.chunk = c => evC.version <= v
이건 내가 봐온 (P => Q && P) => Q류의 성질보다 훨씬 복잡하다! 이유는 해당 시스템에 대응하는 완전한 P 명세가 이미 있었기 때문일 수도 있다. 하지만 Cheng Huang이 이미 명세 전문가라서, 보통 개발자보다 LLM에서 더 많은 걸 뽑아낼 수 있기 때문일 수도 있다. 나도 대체로, 내 고객들보다 LLM을 더 흥미로운 방향으로 유도할 수 있다는 걸 느낀다. 이건 내 현재 생계에는 좋지만, LLM이 형식 방법을 대중화하리라는 희망에는 좋지 않다. LLM에게 형식 방법을 시키려면 형식 방법을 알아야 한다면, 그게 정말 도움이 되는 걸까?
(그래도 도움이 되긴 한다. 기술 임계값을 낮춘다면—80시간 연습해야 하던 걸 20시간으로 줄여준다든가—FM을 적용할 수 있으니까. 하지만 그 임계값을 얼마나 낮추는지는 아직 결론이 나지 않았다. 80을 75로만 낮추는 거라면?)
한편, 어떤 성질은 명시적으로 지시해도 AI가 어려워하는 것 같기도 하다. 지난주에 한 고객과 함께 Claude에게 표준적인 자명한 불변식 대신 괜찮은 liveness나 action 성질을 생성하게 해 보려고 했는데, 그냥 못 했다. 학습 데이터 문제일까? 라이브니스의 고유한 복잡성 때문일까? 아직 확실치 않다. 이런 성질은 대부분의 불변식보다도 더 “미묘”하니, 그 때문일 수도 있다.
또 한편으로는, 이 글은 2026년 3월 기준이다. 6월이 되면 이 글 전체가 우스울 정도로 구식이 되어 있을지도 모른다.
지난주 증정 이벤트에서 몇 가지 문제가 있었다. 첫째, 뉴월드 지역용 책이 이메일이 다 나가기 전에 전부 소진되어서, 많은 사람이 책을 시도해볼 기회조차 없었다. 둘째, Leanpub 버그 때문에 10 AM UTC에 예약한 유럽 쿠폰이 실제로는 내 시간 기준 10 AM에 활성화됐고, 그건 유럽에서는 이른 저녁이었다. 셋째, APAC 지역은 아예 빠졌다.
그래서 다음 주에는 뉴스레터를 쉬는 김에, 증정 이벤트를 한 번 더 하자:
이렇게 하면, 모두가 최소한 책을 시도해볼 기회는 갖게 하면서도 여행/Leanpub의 버그 수정 드랍/서머타임/기타 등등 때문에 생길 수 있는 타임존 장난에도 비교적 튼튼할 거라 생각한다.
(이후의 “뉴스레터 쉬는 주”마다 증정 이벤트가 있을 거라는 보장은 없다! 이건 그냥 gimmick이다)