Formal Specifications & TLA+

1. Overview

정형 명세 및 TLA+(Formal Specifications & TLA+, FST)는 "시스템이 무엇을 해야 하는가"를 자연어의 모호함 없이 수학적 언어로 규정하는 최고의 기술입니다.

특히 Leslie Lamport가 제안한 **TLA+(Temporal Logic of Actions)**는 시간의 흐름에 따른 상태 변화를 집합론과 선형 시간 논리(LTL)로 모델링합니다. 학습자는 시스템의 **불변량(Invariants)**과 생존성(Liveness) 조건을 정의하고, 모델 체커(TLC)를 통해 모든 가능한 실행 경로에서 데드락이나 경쟁 상태(Race Condition)가 발생하지 않음을 물리적으로 검증하는 법을 배웁니다. 이를 통해 초대규모 클라우드 서비스나 복잡한 금융 프로토콜의 설계 단계에서 치명적인 논리 오류를 수리적으로 차단하는 능력을 갖춥니다.

2. Scope & Boundaries

In-Scope

• State Machine Modeling: 시스템 상태와 전이(Transitions)의 수학적 매핑
• TLA+ Syntax: 변수 선언, 초기 상태(Init), 동작(Next) 정의 및 논리 연산자 활용
• Temporal Logic: '항상(Always, □)'과 '결국(Eventually, ◇)'을 이용한 흐름 기술
• Model Checking Mechanics: 상태 공간(State Space) 탐색 및 반례(Counterexample) 생성 원리

Out-of-Scope

• 프로그래밍 언어의 유닛 테스트 코드 작성 (09-02 SDM 영역으로 위임)
• TLA+ 도구 자체의 설치 및 UI 가이드 (도구 사용법 영역)

Boundaries

• FST vs. Testing: 테스트가 '몇 가지 입력'으로 버그를 찾는 것이라면, FST는 '전체 상태 공간'을 수학적으로 뒤져서 논리적 결함의 부존재를 증명합니다.

3. Counterexample

• 단순히 "Flowchart를 그리는 것"은 FST 학습이 아닙니다. 왜 특정 분산 합의 알고리즘에서 안전성(Safety) 조건인 '오직 하나의 리더만 선출됨'이 모든 네트워크 지연 상황에서도 물리적으로 유지되는지 LTL(Temporal Logic) 수식으로 입증하지 못하거나, TLC 모델 체커가 제시한 반례를 보고 시스템의 '중간 상태(Intermediate State)' 누락을 지적하지 못한다면 FST의 본질을 이해하지 못한 것입니다.

4. Prerequisites

• 명제 및 서술어 논리 (Basic): 불 대수와 양화사 사용이 필수입니다. (02-01 PPL)
• 집합론 및 관계 (Recommended): 상태들의 집합과 전이 관계 모델링을 위해 필요합니다. (01-01 STR)

5. Learning Map

1. Declarative Vision: 명령형 코드가 아닌 시스템의 '바람직한 상태'를 선언하는 법을 익힙니다.
2. Action Dynamics: 논리 연산자를 이용해 상태 A에서 B로 이동하는 물리적 제약을 정의합니다.
3. Temporal Invariants: 시간의 흐름 속에서도 절대 깨지면 안 되는 진리(Safety)를 고정합니다.
4. Exhaustive Verification: 모델 체킹을 통해 인간이 상상하지 못한 엣지 케이스 실행 경로를 수학적으로 격파합니다.

6. Learning Topics

Basic

Core: 정형 명세의 기초와 상태 기계 (Formal Foundations)

• Why to Learn: 프로그램 아키텍처를 그리기 전, 논리적 설계에 빈틈이 없는지 확인하기 위함입니다.
• What to Learn:
  • 명세(Specification) vs 구현(Implementation)의 차이점
  • 모듈화된 상태 기계(State Machine)의 물리적 선언
  • 비결정론적(Non-deterministic) 동작의 의미와 모델링
• How to Learn:
  • 신호등 시스템을 빨강/초록/노랑 상태와 전이 조건으로 수학적 모델링 실습
  • 자연어로 된 요구사항 중 모호한 부분(예: "빠른 응답")을 수리적 범위로 치환하는 연습
• Implement: 마이크로서비스의 간단한 상태 전이도를 집합론적 기호로 기술한 명세서

Recommended

Core: TLA+ 언어와 수리 논리 (TLA+ Paradigm)

• Why to Learn: 업계에서 가장 강력한 정형 검증 도구인 TLA+의 언어적 역학을 이해하기 위해서입니다.
• What to Learn:
  • PlusCal과 TLA+의 관계 및 수리적 변환
  • 집합 구조체(RECURSIVE, CHOOSE)를 이용한 복잡 데이터 모델링
  • 동작(Action)의 정의: $Next \triangleq P \vee Q$ 형태의 논리 합 결합
• How to Learn:
  • $2+2$ 가 $4$가 되는 과정을 TLA+의 상태 변화로 정의해 보는 기초 실습
  • "모든 사용자는 고유한 ID를 가진다"를 TLA+의 Invariant 구문으로 작성 연습
• Implement: 생산자-소비자(Producer-Consumer) 패턴의 논리적 무결성을 정의한 TLA+ 파일

Practical

Core: 시간 논리와 안전성/생존성 (Temporal Dynamics)

• Why to Learn: 시스템이 '나쁜 짓을 안 하는 것'과 '좋은 일을 결국 하는 것'을 구분하여 검증하기 위함입니다.
• What to Learn:
  • 안전성(Safety): "나쁜 상태에 절대 도달하지 않음"의 수리 증명 (□ $\neg Error$)
  • 생존성(Liveness): "결국 원하는 상태에 도달함"의 수리 보장 (◇ $Success$)
  • 유한 모델 체킹: 무한한 상태를 검증 가능한 유한 영역으로 압축하는 물리
• How to Learn:
  • 은행 이체 시스템에서 '잔액 0 미만 방지'는 안전성인지 생존성인지 판별 실습
  • TLC 모델 체커의 성능 옵션(Worker 개수 등)에 따른 상태 탐색 효율 물리적 측정
• Implement: 데드락(Deadlock)이 발생하지 않음을 생존성 수식으로 검증한 분산 락(Lock) 모델

Advanced

Core: 분산 알고리즘 검증 실전 (Distributed Verification)

• Why to Learn: Paxos, Raft 등 극도로 정교한 분산 알고리즘의 설계 결함을 찾아내기 위해서입니다.
• What to Learn:
  • 추상화 계층(Refinement): 고수준 명세와 저수준 구현의 논리적 일치성 증명
  • 메시지 패싱(Message Passing)의 비동기적 물리 모델링
  • 네트워크 단절 및 재시작 시나리오의 상태 공간 확장 기법
• How to Learn:
  • AWS S3나 DynamoDB에서 TLA+를 사용해 어떤 버그를 미리 잡았는지 실제 기술 블로그 사례 분석
  • 단순한 분산 카운터 알고리즘을 설계하고, 모델 체킹 중 발견된 '인종 차별(Race)' 조건 수정 실습
• Implement: 다중 노드 합의 알고리즘의 특정 상황(Node Fail)에 대한 검증 명세 모듈

7. Terminology

8. References

Primary

• [P1] CS2023 - DS/Discrete Structures and Modeling — Logic and state machines.
• [P2] SWEBOK v4.0 - Software Requirements / Formal Methods — Industry specs.

Secondary

• [Specifying Systems] Leslie Lamport — The original TLA+ "Bible".
• [Practical TLA+] Hillel Wayne — Modern, engineer-friendly guide.

Industry

• [TLA+ at Amazon Web Services] — Real-world case study on S3/DynamoDB.
• [Microsoft Azure Service Fabric Verification] — Verification of complex cloud fabric.

9. Final Checklist

Primary

• TLA+의 초기 상태($Init$)와 다음 상태($Next$) 수식을 보고 시스템의 전체적인 상태 머신 다이어그램을 역으로 물리적 재현 가능한가? (P1)
• '무한 루프'가 발생하는 코드를 TLA+의 생존성(Liveness) 관점에서 왜 위반인지 수학적으로 설명 가능한가? (P1)

Secondary

• TLC 모델 체커의 오류 보고서(Counterexample Trace)를 보고, 실제 코드에서 어떤 순서로 동작이 꼬였는지 물리적 버그 원인을 특정할 수 있는가?
• PlusCal 알고리즘 언어가 실제 TLA+ 논리 수식으로 어떻게 '동작 전이(Next Action)'로 번역되는지 그 논리 흐름을 소통 가능한가?

Industry

• 새로운 합의 프로토콜이나 분산 트랜잭션 설계 시, TLA+ 모델링을 통해 네트워크 파티션 상황에서도 데이터 일관성이 보장됨을 수리적으로 입증할 수 있는 가? (SFIA)
• 아키텍처 리뷰 단계에서 자연어 명세의 모호함을 지적하고, 정형 명세로 전환했을 때 기대되는 리스크 감소 효과를 정량적으로 제시할 수 있는 가?