Hacker News • 13일 전

LLM 시대의 TLA+ 입문: 프롬프트로 승리하기

IMP

8/10

핵심 요약

TLA+의 복잡한 문법이 LLM(대형 언어 모델) 시대를 맞아 진입 장벽이 크게 낮아졌습니다. 이제 엔지니어는 시스템과 '올바름(Correctness)'을 정의하는 것에 집중하고, 실제 모델 검사(Model Checking) 코드는 프롬프트로 쉽게 생성해 복잡한 분산 시스템이나 알고리즘을 검증할 수 있습니다. 본문은 고전적인 콩 시뮬레이션 문제를 통해 TLA+의 기본 개념과 상태 변환 논리를 설명합니다.

번역된 본문

대부분의 엔지니어들이 TLA+를 사용할 때 처음 하는 불만은 문법이 까다롭다는 것입니다. 코드보다는 LaTeX처럼 보이기 때문입니다. 하지만 이제 최신 LLM(대형 언어 모델)은 TLA+를 쉽게 생성할 수 있습니다. 여전히 시스템을 이해하고 '올바름(Correctness)'이 무엇을 의미하는지 정의하는 것은 개발자의 책임이며, 시제 논리(Temporal logic)에 대한 높은 수준의 이해가 필요합니다. 이 글에서는 시제 논리에 대해 설명하겠습니다. 마지막에는 Claude를 사용해 TLA+ 스펙(Spec)을 시작하는 예시 프롬프트를 보여드리겠습니다. 새로운 글을 보려면 구독하세요.

간단한 예제 문제 # 다음은 고전적인 퍼즐입니다. 콩이 들어있는 통이 있습니다. 각 콩은 흰색 또는 검은색입니다. 통은 처음에 비어있지 않습니다. 콩이 적어도 2개 이상 있는 동안 다음을 반복합니다: 콩 2개를 고릅니다. 두 콩이 같은 색이면: 두 개 모두 버리고, 흰색 콩 1개를 넣습니다. 두 콩이 다른 색이면: 두 개 모두 버리고, 검은색 콩 1개를 넣습니다. 두 가지 질문이 있습니다: 콩의 수가 0이 될 수 있을까요? 알고리즘이 b = 1(검은 콩 1개)로 종료된다면, 처음에는 어떤 상태였어야 할까요?

머리를 쥐어짜며 생각해볼 수도 있습니다. 아니면 이를 TLA+로 작성하고 모델 검사기(Model checker)가 두 질문에 자동으로 답하게 할 수도 있습니다. 이 방법의 핵심은 생각하는 과정을 피하는 것입니다. 적어도 기계가 당신의 생각이 맞았는지 검증하게 만드는 것입니다. 아니면 친구들이나 연구 논문의 동료 평가 위원회(peer-review panel)에게 당신의 생각이 옳다는 것을 납득시키는 것입니다.

논리 공식이 상태 기계(State machine)를 만드는 방법 # TLA+는 1990년대 레슬리 램포트(Leslie Lamport)가 발명했습니다. TLA는 '행동의 시제 논리(Temporal Logic of Actions)'를 의미하며, TLA+는 이 특정 언어의 이름입니다. TLA+는 기본적인 부울 논리(Boolean logic)와 집합(sets), 함수(functions), 한정자(Quantification, '모든 것에 대해(for all)'와 '존재한다(there exists)')를 가지고 있습니다. 또한 곧 보게 될 시제 논리 연산자들도 있습니다.

TLA+로 명세(Specification)를 작성할 때, 당신은 상태 기계를 정의하는 논리 공식을 작성하는 것입니다. 이 기계는 고정된 변수 세트를 가지고 있으며, 각 상태는 변수들에 할당된 값들입니다. 콩 통 문제의 경우, 변수는 w(흰색 콩의 수)와 b(검은색 콩의 수)입니다. 각 상태는 w와 b에 할당된 값입니다. 동작(Behavior)은 상태의 연속이며, 명세는 허용되는 동작들의 집합입니다.

초기 상태 # 우리는 초기 상태 규칙이 필요합니다. 즉, 우리가 시작할 수 있는 상태에만 참으로 평가되는 조건(Predicate)입니다. 영어로는 "통은 초기에 비어있지 않다", 즉 w + b > 0 입니다. 다음 중 이 조건과 일치하는 초기 상태는 어느 것일까요?

b = 0 /\ w = 0 b = 0 /\ w = 4 b = 6 /\ w = 1 b = 1 /\ w = "foo"

TLA+에서 "/"는 "그리고(and)"를 의미하므로, b = 0 /\ w = 0은 "b = 0 그리고 w = 0"을 뜻합니다. 두 번째와 세 번째 상태가 조건과 일치합니다. 첫 번째는 w와 b의 합이 0이므로 일치하지 않고, 마지막 상태는 1과 문자열 "foo"를 더할 수 없으므로 말이 안 됩니다.

TLA+에는 타입 시스템(Type system)이 없고 집합(sets)만 있으므로, w가 문자열이 되는 것을 막을 수 없습니다. 램포트(Lamport)는 이런 상태를 '어리석은(silly)' 것이라고 부릅니다. 우리는 w와 b가 자연수여야 한다고 지정함으로써 이런 어리석은 상태를 방지합니다:

EXTENDS Integers Init == w \in Nat /\ b \in Nat /\ w + b > 0

EXTENDS Integers는 자연수의 집합인 Nat와 같은 정수 처리에 필요한 모든 것을 가져옵니다(import). \in은 집합 소속 연산자(∈)입니다. TLA+에서 ==는 '~로 정의된다'를 의미합니다. 이것은 약간 헷갈릴 수 있는데, C 언어와는 반대 개념이기 때문입니다. 즉, 단일 =는 동등성을 검사(tests for equality)하고, ==는 공식(매크로와 같은)의 이름을 붙입니다.

상태 전이(State transitions) # 상태 전이 규칙은 두 상태(현재와 다음)에 대한 조건(Predicate)으로, 어떤 전이가 유효한지를 나타냅니다. 알고리즘을 TLA+의 상태 전이 규칙으로 바꿔 봅시다. 영어에서 시작해 보겠습니다:

흰색 콩 2개: 흰색 2개를 제거하고, 흰색 1개를 추가 -> 최종 효과: w -= 1 검은색 콩 2개: 검은색 2개를 제거하고, 흰색 1개를 추가 -> 최종 효과: b -= 2 하나씩 있는 경우(다른 색상): 흰색 1개와 검은색 1개를 제거하고, 검은색 1개를 추가 -> 최종 효과: w -= 1

첫 번째와 세 번째 경우가 상태에 미치는 효과가 동일하다는 점을 주목하세요. 둘 다 단순히 w에서 1을 빼고 b는 그대로 둡니다. 이것이 바로 이런 종류의 통찰력입니다.

원문 보기

원문 보기 (영어)

Most engineers’ first objection to using TLA+ is, the syntax is hostile. It looks like LaTeX, not like code. But now, frontier LLMs can generate TLA+ easily. It’s still your responsibility to understand your system and define what “correctness” means, and you need a high-level understanding of temporal logic. I’ll explain temporal logic in this article. At the end I’ll show an example prompt to start a TLA+ spec with Claude. Subscribe for new articles A toy problem # Here’s a classic puzzle. You have a can of beans. Each bean is white or black. The can starts nonempty. While there are at least 2 beans: Choose 2 beans. If they’re the same color: discard both, add 1 white bean. If they’re different colors: discard both, add 1 black bean. Two questions: Can the number of beans ever reach zero? If the algorithm terminates with b = 1, what must have been true at the start? You could think really hard. Or you could write it down in TLA+ and let a model checker answer both questions automatically. The whole point is to avoid thinking—or at least, to have a machine verify that your thinking was correct. Or convince your friends that your thinking is correct, or convince the peer-review panel for your research paper. How logical formulae produce a state machine # TLA+ was invented by Leslie Lamport in the 1990s. TLA stands for “Temporal Logic of Actions,” and TLA+ is the name of the specific language. TLA+ has basic boolean logic, and it has sets and functions, and quantification (“for all” and “there exists”). It also has temporal operators, which we’ll see soon. When you write a specification in TLA+, you’re writing a logical formula which defines a state machine. The machine has a fixed set of variables, and each state is an assignment of values to the variables. For the can problem, there are variables: w (the number of white beans) and b (the number of black beans). Each state is an assignment of values to w and b . A behavior is a sequence of states, and a specification is the set of allowed behaviors. Initial state # We need an initial-state rule—a predicate that’s true of exactly the states we’re willing to start from. In English: “the can is initially nonempty,” or w + b > 0 . Which of these initial states matches the predicate? b = 0 /\ w = 0 b = 0 /\ w = 4 b = 6 /\ w = 1 b = 1 /\ w = "foo" In TLA+ “/\” means “and”, so b = 0 /\ w = 0 means “b = 0 and w = 0”. The second and third states match the predicate. The first doesn’t, because w and b sum to zero, and the final state doesn’t make sense because you can’t add 1 and the string “foo”. TLA+ has no type system, only sets, so there’s nothing stopping w from being a string. Lamport calls something like that “silly.” We prevent silly states by specifying that w and b must be natural numbers: EXTENDS Integers Init == w \in Nat /\ b \in Nat /\ w + b > 0 EXTENDS Integers imports everything you need for handling integers, like the set of natural numbers Nat , and \in is the set-membership operator ∈ \in . In TLA+, == means “defined as.” This is confusing, because it’s kind of the opposite of C: a single = tests for equality, and == names a formula (like a macro). State transitions # A state-transition rule is a predicate over two states—current and next—that says which transitions are legal. Let’s turn our algorithm into a state-transition rule in TLA+. Starting from English: 2 white beans: remove 2 whites, add 1 white → net effect: w -= 1 2 black beans: remove 2 blacks, add 1 white → net effect: b -= 2 1 of each: remove 1 white and 1 black, add 1 black → net effect: w -= 1 Notice the first and third cases have identical effects on the state: both just subtract 1 from w and leave b alone. This is the kind of insight that falls out naturally when you write things down precisely. In TLA+ these become three actions : WW == w > 1 /\ w' = w - 1 /\ UNCHANGED b \* Picked 2 white BB == b > 1 /\ b' = b - 2 /\ w' = w + 1 \* Picked 2 black WB == w > 0 /\ b > 0 /\ w' = w - 1 /\ UNCHANGED b \* Picked 1 of each There are two operators that we’re seeing for the first time here. The prime ( ' ) operator means “the next value of this variable”: w' = w - 1 means “in the next state, w will equal the current w minus 1.” UNCHANGED b is shorthand for b' = b . You have to account for every variable in every action—TLA+ won’t assume that unmentioned variables stay the same. This is annoying, but it forces you to think about what each action does to the whole state. The terms without primes are the guard : conditions that must hold now for the action to fire. The terms with primes are the assignment : what the next state looks like. If the guard is false, the action is disabled. The \* starts a comment (yes, it’s a backslash and a star). A full TLA+ spec # Here’s the full specification: -------------- MODULE beans ----------------- EXTENDS Integers VARIABLES w, b vars == <<w, b>> \* convenient list of all variables Init == w \in Nat /\ b \in Nat /\ w + b > 0 WW == w > 1 /\ w' = w - 1 /\ UNCHANGED b \* Picked 2 white BB == b > 1 /\ b' = b - 2 /\ w' = w + 1 \* Picked 2 black WB == w > 0 /\ b > 0 /\ w' = w - 1 /\ UNCHANGED b \* Picked 1 of each Next == WW \/ BB \/ WB Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ============================================== The formula Next is defined as the OR ( \/ ) of all three actions—at any given state, whichever actions have their guards satisfied are enabled. This is nondeterminism : the spec doesn’t say which action happens, just which are possible. The model checker explores all of them. The Spec line is the spine of any TLA+ specification and you’ll see it in basically every TLA+ spec you read. It says: “every behavior allowed by this spec starts from an initial state where Init is true, and every transition satisfies Next.” The WF_vars(Next) part means “the algorithm must keep making progress—it can’t stall forever when an action is enabled.” That’s called a fairness constraint , stay tuned… The [][Next]_vars part hides some complexity I’m going to skip. If you want to deeply understand it, read Lamport’s “Specifying Systems.” For prompting purposes, just know it goes there. States and behaviors # A behavior is an infinite sequence of states, starting from an initial state, where each step is allowed by Next . Behaviors are infinitely long by convention. If the algorithm terminates (reaches a state where no further actions are enabled), the final state just repeats forever. That repetition is called stuttering . So “termination” in TLA+ means the algorithm reaches a stuttering state and stays there. There are infinitely many init states in our spec—any pair of natural numbers with w + b > 0 is a valid initial state. Let’s look at a subset of the state space, just the states that begin at b=3 and w=5: Each node is a state. Each edge is a valid transition, labeled with which action(s) apply. Some edges say “WW/WB”—that’s because when w > 1 and b > 0 , both WW and WB are enabled and lead to the same next state (both just decrement w by 1). The model checker explores both actions but discovers the same successor state, so they collapse into one edge. A behavior in this picture is a path from the initial node to a terminal node, followed by stuttering. Here’s a behavior: Model-checking # The model-checker, TLC, starts from the set of initial states, applies the next-state relation to generate successor states, and uses hashing (it calls this “fingerprinting”) to avoid revisiting states it’s already seen. As TLC disco

TLA+ 형식명세 대형언어모델 소프트웨어검증 모델검사