Formal methods with Hillel Wayne

메타데이터

• 채널: The Pragmatic Engineer (Gergely Orosz)
• 제목: Formal methods with Hillel Wayne
• URL: https://www.youtube.com/watch?v=KSkcgIYQy0U
• 영상 길이: 약 85분 (5093초)
• 처리일: 2026-07-31
• 게스트: Hillel Wayne (formal methods 컨설턴트, TLA+ 강사, 『Logic for Programmers』 저자, 곧 Antithesis 합류 예정)

---

1. 핵심 요약

이 에피소드는 "AI가 코드를 더 많이 짤수록, formal verification(정형 검증)이 주류가 될 것"이라는 최근 업계의 낙관론에 대해, 실제 formal methods 전문가 Hillel Wayne이 직접 답하는 자리다. 결론부터 말하면 **"제대로 된 formal methods는 대부분의 경우 오버킬이지만, 라이트웨이트한 formal methods(예: property-based testing)는 실제로 유용해질 것"**이라는 것이 Hillel의 결론이다.

에피소드는 크게 세 파트로 구성된다.

1. 크로스오버 프로젝트: "소프트웨어 엔지니어는 진짜 엔지니어인가?"를 다른 공학 분야(광산, 화학, 전기, 토목 등) 15~20명 인터뷰로 검증한 Hillel의 과거 프로젝트 회고
2. Formal methods 실전 데모: TLA+, Alloy, property-based testing(hypothesis)을 직접 라이브 데모로 보여주며 각각의 작동 원리와 실제로 발견한 버그 사례를 설명
3. AI 시대의 formal methods: AI가 스펙(specification) 문법 수정·에러 트레이스 해석·보일러플레이트 작업은 잘하지만, **"properties(속성)를 스스로 고안하는 것"**에는 여전히 매우 약하다는 실측 경험 공유

핵심 메시지: formal methods의 병목은 "증명 자체"가 아니라 "무엇을 증명해야 하는가(spec)를 정확히 정의하는 것"이며, 이 부분이야말로 AI가 아직 가장 취약한 영역이다.

---

2. 주요 발언 / 근거

Hillel Wayne의 커리어 배경

• 대학에서 물리학/수학을 전공하려 했으나 "물리학 자체를 즐기지 못한다"는 걸 깨닫고, 실험실에서 하던 프로그래밍이 제일 재밌었다는 걸 발견
• 샌프란시스코에서 Ruby on Rails 개발자(에듀테크)로 커리어 시작 → 시카고로 돌아와 에듀테크 회사에서 일하다 formal verification/formal methods라는 니치에 빠짐

"왜 formal methods를 모든 곳에 쓰지 않는가?" (핵심 논증)

"When you start talking about like most interesting domain problems, you have to pull in so much context that basically even writing what the function is supposed to do becomes a nightmare. The imperative program you write that will get correct 99% of the time is probably good enough to use in almost all cases."

• 예시: "리스트에서 가장 큰 수를 찾아라" → 쉽게 스펙 작성 가능
• 그러나 "디렉토리에서 가장 줄 수가 많은 파일을 찾아라" → ASCII 줄바꿈이냐 UTF-8이냐, 권한 없는 파일은 무시하냐 에러내야 하냐, 심볼릭 링크는 어떻게 하냐, 디렉토리인 경우는? → "You're now simulating real world"
• 즉 도메인이 복잡해질수록 "무엇이 옳은가"를 formal하게 정의하는 것 자체가 실질적으로 불가능에 가까워짐

Formal methods가 실제로 쓰이는 3가지 카테고리

1. 원자력/NASA급 초고신뢰 시스템 — 의외로 원자력 발전소는 이 정도까지는 안 쓰고 철저한 테스팅으로 충분하다고 여김
2. 핵심 코어 컴포넌트만 검증 — 데이터베이스 일부, 암호화 프리미티브(cryptographic primitives), Firefox의 HTTPS 스택(Project Everest), seL4(마이크로커널, Isabelle로 end-to-end 검증, 자동차/군사용)
3. Hillel 본인의 영역: 시스템의 단순화된 모델을 만들어 검증 — 실제 시스템 전체가 아니라 추상화된 버전을 stress-test해서 설계 단계의 버그를 미리 걸러냄 (주로 데이터베이스, 분산 시스템, 열차 신호 시스템(transponder) 등)

AWS와 TLA+ (2014년 논문)

"The shortest error trace exhibiting the bug contained 35 high-level steps" — 인간이 손으로 추적하기 사실상 불가능한 깊이

• 2014년 "Use of Formal Methods at Amazon Web Services" 논문에서 AWS 엔지니어 일부가 TLA+와 PlusCal을 독학해서 DynamoDB, S3 스토리지 시스템에 적용
• 데이터 유실로 이어질 수 있는 복잡한 replication 버그를 발견
• Hillel의 추정: 상태공간(state space)이 1억 개 규모였을 것이므로, 35단계짜리 버그를 인간이 수동으로 찾는 건 사실상 불가능

동시성(concurrency) 버그가 어려운 진짜 이유 — "연습 부족"

"Usually when you have a race condition in a system, you find out months later and then you try a fix and you find out weeks later after that if the fix actually worked. Whereas with TLA+ I write my model of the system and then I click a button and it immediately tells me hey race condition..."

• Hillel은 동시성 자체가 인간에게 본질적으로 어려운 게 아니라고 주장 — 길 건널 때 우리는 이미 "동시에 여러 차가 움직이는 시스템"을 직관적으로 다루고 있음
• 근거 논문: "Common Sense Computing" — 동시성 문제를 "여러 스레드가 작업을 수행한다"는 식으로 제시하면 어려워하지만, "콘서트 좌석을 배정하는 매표소 직원 여러 명"으로 바꿔 제시하면 버그를 훨씬 빨리 찾아냄
• 실무에서 레이스 컨디션은 몇 달~몇 년에 한 번 겪기 때문에 전문성이 쌓이기 어려움. TLA+는 즉각적인 피드백 루프(모델 작성 → 클릭 → 즉시 버그 발견/수정 → 재확인)를 제공해 이 "연습 부족" 문제를 해결

Time-to-check / Time-to-use 버그 패턴

• 검증 시점과 사용 시점 사이에 상태가 바뀌는 클래식 버그. 은행 계좌 이체 예시로 설명: "$10 있는지 확인 → 있음 → 그런데 확인과 인출 사이에 다른 프로세스가 그 $10을 먼저 가져가버림 → 잔액이 마이너스가 됨"
• Gergely는 Uber 결제 시스템 구축 경험을 연결: "exactly-once delivery"가 "at-least-once delivery"보다 훨씬 어려운 이유, 그리고 호텔이 신용카드를 더 큰 금액으로 선(先)승인하는 이유(엣지케이스 회피)

TLA+ 라이브 데모 — 거래 플랫폼 버그

• Leslie Lamport(LaTeX 창시자와 동일 인물)가 1994년 만든 TLA+(Temporal Logic of Actions)
• 데모 시나리오: Alice, Bob, Carol이 스틱(아이템) 1개를 거래. Alice가 Bob에게 제안 → Bob이 응답 없음 → Alice가 Carol에게도 제안 → Carol이 즉시 수락(스틱이 Alice→Carol로 이동) → 뒤늦게 Bob이 (이미 무효가 된) 원래 제안을 수락 → 시스템이 "스틱이 Carol→Bob으로 이동했지만 Carol이 Bob에게 제안한 적이 없다"는 불변식(invariant) 위반을 자동으로 검출
• 53개 state 만에 버그 발견. "Change invariant(변경 불변식)"이 위반된 경로를 정확히 재현해서 보여줌
• TLA+는 상태 공간(state space)을 브루트포스로 전수 탐색 — 프로세스가 여러 개일 때 "프로세스1이 스텝1을 밟고, 프로세스2가 스텝1, 프로세스1이 스텝2..." 식의 모든 인터리빙 조합을 사람이 손으로 검토하는 건 불가능하지만 컴퓨터는 밤새 브루트포스로 처리 가능

Alloy 데모 — 접근 제어(access control) 시스템 버그

• MIT 교수가 만든 Alloy — TLA+와 다른 계보(lineage)의 formal spec 툴
• 시나리오: 리소스에 "읽기 권한을 가진 사용자" 목록 + 부모-자식 관계. "부모를 읽을 수 있으면 자식도 읽을 수 있다"는 속성을 명시했다고 착각했지만 실제로는 readable-by가 전이적(transitive)이지 않음 — 부모의 자식은 읽을 수 있지만, 자식의 자식(손자)은 못 읽는 버그
• Alloy는 SAT solver(SAT4J)를 이용해 boolean satisfiability 문제로 변환 — TLA+가 브루트포스로 밤새 걸리는 것과 달리 Alloy 모델은 대부분 몇 밀리초~1초 내에 체크 가능
• 수정 방법을 formal methods가 정해주지는 않는다 — "이행적 클로저(transitive closure)로 고치자"는 아이디어는 나오지만, 실제 SQL DB에서 구현 가능한지(성능 문제 등)는 별개 문제로 다시 논의해야 함

기타 formal methods 툴 생태계 (Hillel이 언급한 목록)

• 모델 명세용: TLA+, PlusCal, P(Microsoft Research 출신, Amazon으로 이직한 사람이 개발, TLA+보다 접근성 높음, actor model과 유사), Quint(TLA+에서 파생, 은행/암호화폐 스마트컨트랙트 업계에서 관심), Prism(확률적 모델 체커 — "이 버그가 10% 확률로 발생한다" 같은 걸 말해줌, TLA+는 불가능), Event B(파리 지하철 시스템에 사용된 이력), mCRL2(네덜란드 대학), UPPAAL(로봇 제어), NuSMV(NASA 사용)
• 코드 검증용: Dafny(.NET 컴파일, 증명 가능한 코드 작성), JML(Java), Frama-C(C), Ada SPARK, 정리증명기(theorem prover)인 Coq, Lean, Isabelle
• 각 툴은 강점이 다름 — TLA+는 이산적(discrete) 분산 시스템에 강하지만 부동소수점/확률적 추론은 못함

Property-based testing 데모 (hypothesis, Python)

• Hillel의 책에 나오는 예시: max(list) 함수의 3가지 버전(정상 버전, 처음 3개만 보는 버그 버전, 절댓값 기준 버그 버전)
• 스펙: "리스트의 최댓값은 리스트 안에 있어야 하고, 다른 모든 원소보다 크거나 같아야 한다"
• Formal methods는 "모든 가능한 리스트에 대해" 증명하려 하지만, property-based testing은 대신 수천 개의 랜덤 리스트를 생성해서 테스트 — 완전성은 떨어지지만 실무 적용이 훨씬 쉬움
• hypothesis 라이브러리는 실패 사례를 찾으면 "최소한으로 흥미로운(minimally interesting) 예제"로 자동 축소(shrinking)해서 사람이 이해하기 쉬운 형태로 제시
• Hillel의 결론: "formal methods는 니치 툴이지만 property-based testing은 훨씬 더 많은 사람에게 유용할 중간지대(middle ground)다"

AI와 formal methods — 실측 경험

"I think the one thing AI is extremely bad at ... It is very bad at coming up with properties. ... if you basically tell it 'here's a spec, also come up with the properties of the spec,' it'll be like, 'okay, so one of the properties I'm going to specify is that either P is true or not P is true.' And you're like, that's just always true. And it's like, 'wow, I verified it. Amazing.'"

• AI가 잘하는 것: 문법 오류 수정, 35단계짜리 에러 트레이스를 2문단짜리 영어로 요약, 보일러플레이트 대량 수정, 매우 정밀한 영어 설명을 스펙으로 번역
• AI가 못하는 것: 스펙 자체를 고치는 것, 특히 properties(무엇을 검증해야 하는가)를 스스로 고안하는 것 — 특히 liveness property(시스템이 장기간 어떻게 진화하는가에 대한 속성)에서 취약
• 이 판단은 2025년 6월 뉴스레터에서 이미 밝혔던 것과 2026년 3월 현재도 일관됨(Claude 4.8 출시 시점에도 동일)
• 예외 사례: Chang Huang(GitHub Copilot팀 엔지니어)이 Azure Storage 프로덕션 소스코드에서 AI로 TLA+ 스펙을 자동 생성해 레이스 컨디션을 발견한 사례(2025년 3월 블로그, Lampport Agent 툴) — 단, 이 사람은 이미 숙련된 스페시파이어(specifier)였고, 대상 시스템도 이미 P 언어로 정교한 스펙이 있었다는 전제조건이 있었음
• Claudia Collie(중국 대형 클라우드 업체에서 수년간 formal methods 프로젝트 수행)의 관찰: 논문 작성 기간 동안 LLM이 발전하면서 스펙 작성에 걸리는 시간이 극적으로 압축됨
• Hillel의 결론: "AI가 formal verification을 대중화(mainstream)까지는 못 만들지만, 0.1%에서 0.3%로 늘리는 정도는 가능" — 여전히 이미 formal methods를 아는 전문가들이 AI를 증폭기로 쓰는 패턴이 대부분

"왜 formal methods를 배워야 하는가" (AI 시대에도)

"You need to be able to tell when the AI is doing something wrong, right? And if you don't know the basics, you can't really do that very well."

• AI를 formal methods에 활용하려 해도 기초는 필요 — AI 출력이 틀렸는지 판단할 수 있어야 하기 때문

---

3. 세부 내용 / 사례

크로스오버 프로젝트 — "소프트웨어 엔지니어는 진짜 엔지니어인가?"

• 계기: Glenn Vanderburg의 강연에서 "다른 공학과 소프트웨어가 실제로 매우 유사하다"는 주장을 접하고 회의적이었으나, 직접 15~20명(약 6~7개 공학 분야)을 인터뷰해서 검증하기로 함
• 결론: 5년 전 이 프로젝트를 마쳤을 때는 "확신 없음"이었지만, 지금은 "우리는 엔지니어가 맞다"는 쪽으로 완전히 기울었음(단, LLM 이전 시점 기준의 결론이며 LLM이 이 계산을 어떻게 바꿨는지는 별도 문제라고 단서를 닮)

공통점

• 모든 엔지니어링 분야가 waterfall을 싫어함 — 핵심 긴장관계는 "실수 비용" vs "반복 속도": 반복이 빠를수록 사전 계획이 덜 필요하고, 실수 비용이 높을수록 계획이 더 필요
• 광산 엔지니어링도 1960년대에 "애자일 혁명"(New Austrian Tunnelling Method)을 겪음 — 빠르게 변화를 주고 시스템 반응을 보며 코스 수정하는 방식
• 버전 관리 — 인터뷰한 20명 전원이 "우리 분야에도 있었으면 좋겠다"고 답한 유일한 항목. 소프트웨어의 버전 관리는 "모델 T와 현대 자동차" 수준의 차이로 다른 분야를 압도
• 오픈소스 문화 — 소프트웨어만이 가진 독특한 특성. 다른 분야는 학술 컨퍼런스와 벤더 트레이드쇼 두 종류만 있지만, 소프트웨어는 "practitioner conference"(실무자들이 그냥 더 잘하려고 모이는 컨퍼런스)라는 제3의 형태가 있음. Hillel의 가설: 소프트웨어는 "만드는 재료"와 "만들어지는 결과물"이 동일(코드로 코드를 만듦)하기 때문에 공유가 쉬움

차이점

• 소프트웨어는 변동성(variance)이 거의 없음 — CPU 저항값 스펙시트는 "20~50도 사이에서 100옴의 ±20% 편차"를 명시하지만, 소프트웨어는 (CPU 버그가 없는 한) 어느 컴퓨터에서 돌려도 동일하게 동작. 소프트웨어의 "변동성"은 순전히 우리가 스스로 만든 것(다양한 API, 칩셋, 포트 등)
• 화학공학은 밤새 실험을 돌려 다음날 결과를 봄 — "빠르다"고 여겨지지만, 소프트웨어는 F11 한 번으로 즉시 결과를 봄 → 반복 속도에서 소프트웨어가 압도적
• 소프트웨어가 다른 분야에서 배울 점: (1) 반복은 잘하지만 계획(planning)은 상대적으로 약함, (2) 재료(오픈소스) 공유는 잘하지만 "직무의 구체적 노하우"를 체계적으로 정리하는 문화는 약함 — 예시로 "스냅핏 핸드북"(500쪽짜리, 리모컨 배터리 뚜껑의 클릭 방식만 다루는 책)을 언급하며 "API 버저닝에 대한 500쪽짜리 책 같은 게 소프트웨어엔 없다"고 지적

수학과 프로그래밍

• 모든 사람에게 필요한 수학(카운팅, 크기 비교)과 특정 직군에만 필요한 수학(SRE의 미적분 등)을 구분해야 함
• 그래프/방향그래프, 행렬, 형식논리(formal logic)는 폭넓게 유용한 중간 영역
• 전통 공학 대부분은 연속수학(미분방정식, 미적분)을 쓰지만, 소프트웨어/CS는 이산수학(조합론, 그래프이론, 형식논리, 집합론)을 씀 — 미국 고교/대학 초반 커리큘럼은 연속수학 중심이라, 개발자들이 "자신에게 필요한 수학"을 접해본 적이 없어서 수학의 유용성을 못 느끼는 것일 수 있다는 가설

책 추천 (Hillel)

1. 『Engineering a Safer World』 — Nancy Leveson(항공우주 엔지니어, 챌린저 사고·콜롬비아 참사 조사 참여), 무료로 온라인에서 구할 수 있음
2. 『Data and Reality』 — Bill Kent, IBM 데이터베이스 설계자. "데이터란 무엇인가", "정체성/동일성이란 무엇인가"를 다룬 책 (2판이 최선, 재출간판은 내용이 바뀜). "데이터는 현실이 아니라, 우리의 유용한 목적을 위한 현실의 관점(view)이다"
3. 『Debugging: The Nine Indispensable Rules』 — David Agans, 디버깅을 하나의 규율(discipline)로 다루는 몇 안 되는 책. 주니어 엔지니어에게 항상 선물하는 책

1년 전 예측 재검토 (VC/AI 시대 소프트웨어 엔지니어링)

Hillel이 1년 전 작성한 6가지 명제를 하나씩 재검토:

1. "바이브코더는 경력 엔지니어만큼 좋아질 수 없다" — 여전히 맞다고 봄(기초가 없으면 안 됨)
2. "LLM은 전문 엔지니어의 능력을 크게 증폭시킬 수 있다" — 맞음. 깊은 지식을 가진 엔지니어가 AI 툴을 잘 다룰수록 압도적으로 효율적
3. "LLM이 많은 개발자의 일자리를 없앨 것이다" — 판단 어려움. 최근 미국 SW 채용 회복세, 최근 몇 년의 감소는 AI보다 저금리 종료·코로나 이후 조정 효과가 더 컸을 가능성 (Pragmatic Engineer 데이터 언급: 미국/독일/프랑스는 채용 증가, 프론트엔드·모바일 채용은 감소, "AI 엔지니어링"으로 스킬셋 이동 중)
4. "많은(어쩌면 더 많은) 새 개발자 일자리가 열릴 것이다" — 맞다고 봄(1명이 5명분 산출 → 오히려 더 채용하려는 유인)
5. "LLM이 만드는 SW 일자리는 2008~2022년 호황기보다 급여가 낮고 안정성이 떨어질 것" — Hillel이 가장 두려워하는 지점. "다른 어떤 공학 분야가 부다페스트까지 사람을 보내 45분 강연을 시키는가"라며 지금의 소프트웨어 엔지니어링 특권을 잃는 것에 대한 두려움 토로 (투자은행 트레이더 직군의 축소·고급화 사례와 비교됨)
6. "그래도 고임금 전문 SW 엔지니어 일자리는 남겠지만, 더 희소하고 경쟁적이고 개발자 친화적이지 않게 될 것" — 이미 그런 징후가 보인다고 봄. "모든 직업은 시간이 지나며 옥시파이(oxify, 표준화·평준화)되는데, 소프트웨어는 오래 그걸 피해왔을 뿐"

클로징 — 상반된 두 시각의 공존

• Grady Booch가 Gergely에게 한 이야기: 지금 이 시기가 1960~70년대 초 개인용 컴퓨터가 보급되던 시절과 닮았다 — 교사 등 비전문가들도 컴퓨터를 사서 해킹하며 배우던 "민주화"의 시대
• Hillel의 의사 친구 사례: 코드를 전혀 모르는 의사가 AI로 병원 근무 스케줄 교환 플랫폼을 직접 만들어 동료들의 삶을 개선함 — "내 안락한 직업"과 "그의 병원 삶 개선" 사이에서 무엇이 더 중요한지 균형잡기 어렵다는 솔직한 고백
• Clay Shirky의 에세이 "Situated Software" 언급 — 소수의 가족/커뮤니티/학교를 위한 소프트웨어가 이제 코딩 전문가 없이도 가능해지는 시대의 도래

---

4. 시사점

1. Formal methods의 실질적 병목은 "증명"이 아니라 "스펙 정의"다. AI가 아무리 발전해도 "무엇이 옳은 동작인가"를 정의하는 일(properties 고안)은 여전히 사람의 도메인 판단력이 필요한 영역으로 남아있다. 이는 AI 코드 생성 시대에 "코드 리뷰보다 요구사항/의도 정의가 더 중요해진다"는 흐름과 정확히 맞닿아 있다.

2. 일반 엔지니어에게는 formal methods(TLA+ 등)보다 property-based testing이 더 현실적인 채택 대상이다. 완전성은 낮지만 학습 곡선이 훨씬 낮고, "무작위 입력 생성 + 실패 케이스 자동 축소"라는 실용적 가치를 즉시 제공한다. 팀에 도입한다면 TLA+ 같은 풀 스펙 언어보다 hypothesis(Python), fast-check(JS) 같은 property-based testing 라이브러리부터 시작하는 게 ROI가 높다.

3. 동시성/레이스 컨디션에 강해지려면 "의도적으로 자주 마주치는 연습"이 필요하다. 실무에서는 몇 년에 한 번 마주치기 때문에 전문성이 쌓이기 어렵다는 지적은, 팀 차원에서 모델 체킹 도구나 카오스 엔지니어링(예: Antithesis 같은 deterministic simulation testing)을 의도적으로 도입해 "빠른 피드백 루프"를 만드는 것이 학습 효율을 극적으로 높일 수 있음을 시사한다.

4. AI 시대에도 formal methods 기초 지식이 여전히 가치가 있다 — AI가 만들어낸 결과가 맞는지 판단하려면 기본기가 필요하다는 원칙은 formal methods뿐 아니라 코드 리뷰, 아키텍처 설계 등 다른 영역에도 그대로 적용된다. "AI가 다 해주니 기초를 몰라도 된다"는 가정은 최소한 이 분야에서는 아직 틀렸다.

5. 소프트웨어 엔지니어링의 "특권"(고임금, 낮은 진입장벽, 강한 협상력)이 구조적으로 축소될 수 있다는 우려는 진지하게 받아들일 만하다. 투자은행 트레이더 직군의 역사적 궤적(소수화·고급화)과의 비교는, 현재 시니어/전문 엔지니어들에게는 오히려 기회일 수 있지만 주니어 진입장벽이 높아질 가능성을 시사한다 — 커리어 전략 측면에서 "AI로 증폭 가능한 깊은 전문성"을 갖추는 방향이 유효해 보인다.

6. 소프트웨어 엔지니어링을 다른 공학 분야와 비교하는 관점 자체가 유용하다. 버전 관리와 오픈소스 문화라는, 당연하게 여겨온 두 가지가 사실 소프트웨어만의 독특한 특권이라는 인식은 우리가 얼마나 특수한 환경에서 일하고 있는지를 재확인시켜준다.