Skip to content
Published on

Lean 4 & 정리 증명기 2026 — mathlib / Rocq (구 Coq) / Agda / Isabelle / FStar / AlphaProof / AIMO 심층 가이드

🇰🇷KO🇺🇸EN🇯🇵JA
Split View필사 모드
Authors

1장 · 2026년 정리 증명기 지도 — 6개 진영의 풍경

2026년, 정리 증명기(proof assistant, theorem prover) 생태계는 그 어느 때보다 활기차다. 10년 전 "수학자들의 장난감"이라 불리던 도구들이, 지금은 세계 최고 수학자들의 일상 노트북이자 OS 커널과 암호 라이브러리의 안전성 보증서가 되었다.

지금 이 순간 살아있는 주요 진영은 다음과 같다.

진영핵심만든 사람색깔
Lean 4mathlib (1M+ 정리)Leonardo de Moura (AWS)수학 중심, 폭발 성장
Rocq (구 Coq)25년 역사, CompCertINRIA (프랑스)클래식, 산업 검증
Agda의존적 타입의 표본Chalmers (스웨덴)학술/타입이론
Idris 2프로그래밍 우선Edwin Brady실용 의존타입
Isabelle/HOLseL4를 증명함Cambridge / TUM고전 HOL, 자동화 강함
F (FStar)*HACL* 암호 검증Microsoft Research실용 + Z3 결합
Liquid Haskellrefinement typesUCSDHaskell 위 SMT

여기에 더해 두 가지 흐름이 2026년의 공기를 바꾸고 있다.

  1. AI 보조 — DeepMind AlphaProof가 IMO 2024에서 은메달 점수(7문제 중 4문제, 28/42점)를 받았고, Anthropic은 AI Mathematical Olympiad($5M 상금)와 mathlib 검색·자동 증명에 참여했다. Claude·GPT 계열 LLM은 Lean tactic 생성기로 일상적으로 쓰인다.
  2. 현역 일류 수학자의 합류 — Terence Tao(필즈상 2006)는 자기 논문(예: PFR conjecture)을 Lean으로 형식화하는 프로젝트를 공개적으로 진행 중이고, Kevin Buzzard(Imperial College)는 "수학과 학부생이 Lean을 배워야 한다"고 공개 강연한다.

이 글은 위 7개 진영을 한 장씩, 그 다음 AI·SMT·산업 사례를 차례로 짚는다.

용어: proof assistant = "수학자가 증명을 쓰고 컴퓨터가 한 줄씩 검증하는" 도구. SMT solver = "수식이 참인지 자동으로 푸는" 백엔드 엔진(Z3, CVC5). 둘이 합쳐지면 F*나 Liquid Haskell처럼 일반 코드도 검증할 수 있다.

2장 · Lean 4 — Leonardo de Moura, AWS, 폭발 성장

Lean의 짧은 역사

Lean은 Microsoft Research에서 Leonardo de Moura(Z3의 그 사람)가 2013년에 시작한 프로젝트다. Lean 2(2015), Lean 3(2017)을 거쳐 Lean 4가 2021년에 안정화되었다. 2023년 de Moura는 Microsoft를 떠나 Amazon Web Services의 Automated Reasoning Group에 합류했다. AWS는 Lean 4 컴파일러 개발과 mathlib 인프라를 후원한다.

Lean 4의 정체성

Lean 4는 단순한 정리 증명기가 아니라 완전한 의존타입 함수형 프로그래밍 언어다.

-- 자연수 덧셈의 가환성
theorem add_comm (a b : Nat) : a + b = b + a := by
  induction b with
  | zero => simp
  | succ b ih => rw [Nat.add_succ, ih, Nat.succ_add]

theorem은 명제, :=는 증명이다. by ... 블록 안에서 induction, simp, rw(rewrite) 같은 tactic을 호출해 한 단계씩 목표를 해결한다.

Lean 4가 빠른 이유

  • 자체 컴파일러: Lean 4 자체가 Lean으로 작성되었다(self-hosting). C로 컴파일되어 native 성능을 낸다.
  • 매크로 시스템: Racket 스타일의 매크로로 도메인 특화 문법을 사용자가 만들 수 있다. mathlib는 이를 사용해 수학 표기를 그대로 쓴다.
  • 타입 클래스: Haskell 스타일 타입 클래스로 추상화가 깔끔하다.

설치와 첫 증명

# elan: Lean 버전 매니저 (rustup 같은 것)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# 새 프로젝트
lake new my_first_lean
cd my_first_lean
lake build

VS Code에 Lean 4 익스텐션을 설치하면 마우스 hover로 현재 goal과 타입을 실시간으로 본다. 이 InfoView가 Lean 사용자가 사랑하는 첫 번째 이유다.

2026년 현재 상태

  • Lean 4.10+ 안정
  • mathlib는 100만 개 정리 돌파 (다음 장)
  • 학부 강의 채택: Imperial College, Brown, Berkeley, CMU
  • 산업: AWS Automated Reasoning, Galois, Kestrel Institute

Lean Community 사이트 leanprover-community.github.io와 Zulip 채팅은 사실상 24/7 살아있다. 질문을 올리면 보통 한 시간 안에 누군가 답한다.

3장 · mathlib — 100만 정리, Terence Tao의 노트북

mathlib란 무엇인가

mathlib4(Lean 4용)는 인류 역사상 가장 큰 형식화된 수학 라이브러리다. 2026년 5월 현재:

  • 1,000,000+ 정리 (theorem/lemma/def 합산, 2026년 초 돌파)
  • 약 30만 줄의 정의, 80만 줄의 증명
  • 600+ 명의 기여자 (git log)
  • 그룹, 환, 체, 위상, 측도, 범주, 해석, 대수기하…거의 모든 학부+대학원 수학

구조와 표기

import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.MeasureTheory.Integral.SetIntegral

-- 실해석학: 적분의 단조성
theorem integral_mono (f g : ℝ → ℝ)
    (hf : Integrable f) (hg : Integrable g)
    (h : ∀ x, f x ≤ g x) :
    ∫ x, f x ≤ ∫ x, g x := by
  exact MeasureTheory.integral_mono hf hg h

이렇게 일반 수학과 거의 같은 표기를 쓰는 것이 mathlib의 핵심이다. ℝ, ∫, ≤는 그냥 유니코드 글자다. Lean 4의 매크로 시스템이 이걸 가능하게 한다.

Terence Tao와 PFR Project

2023년 11월, Terence Tao(필즈상)는 Tim Gowers, Ben Green, Freddie Manners와 함께 증명한 Polynomial Freiman-Ruzsa 추측 정리를 3주 만에 Lean으로 형식화하는 프로젝트를 시작했다. 결과는 그가 자기 블로그(terrytao.wordpress.com)에 공개적으로 기록했다.

핵심 메시지: "이제 수학자가 형식화에 한 달도 안 걸리고, AI 보조가 점점 더 많이 한다."

2026년 현재 Tao는 자기의 새 논문들 일부를 처음부터 Lean으로 작성하기 시작했다.

누가 mathlib에 기여하는가

  • Imperial College (Kevin Buzzard 그룹)
  • Brown University (Heather Macbeth)
  • 카네기멜런 (Jeremy Avigad)
  • 다수의 PhD 학생, 학부생, 취미 수학자
  • 점차 AI 보조 (다음 장에서)

첫 PR 가이드

mathlib는 진입장벽이 낮다. 처음 기여하는 사람을 위한 가이드와 contribute 페이지가 있다. 정리 하나, 정의 하나, 보조 보조정리 하나도 환영이다.

4장 · Rocq (구 Coq, 2024.3 리브랜드) — 25년의 클래식

왜 이름이 바뀌었나

2024년 3월, Coq 개발팀은 공식 발표로 Coq를 Rocq로 리브랜드한다고 밝혔다. 이유는 두 가지로 요약된다.

  1. "Coq"라는 단어가 일부 언어에서 외설적인 의미로 들려 신규 사용자 진입에 장벽이 됨
  2. 새 세대의 정체성 — Lean이 사용자를 끌어가는 와중에 Rocq 자신을 재정의할 시점

이름은 coq.inria.fr 도메인을 거쳐 rocq-prover.org로 옮겨갔다. 코드 베이스 자체는 그대로 25년 역사를 이어간다(Coq 1.0이 1989년).

Rocq의 강점

  • 튼튼한 산업 검증 기록 — CompCert(아래), seL4 보조, Verdi(분산시스템), CertiCrypt, Iris 등
  • Coq Standard Library가 매우 안정적
  • Ssreflect / mathcomp — Gonthier가 4색 정리, Feit–Thompson 정리(255쪽)를 증명할 때 만든 strategy 라이브러리. Lean의 mathlib보다 오래되었다.
  • OCaml 기반 — INRIA의 OCaml 생태계와 단단히 연결됨

짧은 Rocq 예시

Theorem add_comm : forall a b : nat, a + b = b + a.
Proof.
  intros a b.
  induction a as [| a' IH].
  - simpl. rewrite <- plus_n_O. reflexivity.
  - simpl. rewrite IH. rewrite plus_n_Sm. reflexivity.
Qed.

intros, induction, simpl, rewrite, reflexivity. Lean과 모양은 비슷하지만 문법이 더 LISP스럽다(Qed.로 닫기).

2026년 Rocq vs Lean

항목RocqLean 4
역사1989~2013~
라이브러리mathcomp, stdlibmathlib (1M+)
신규 채택정체 / 감소폭발 성장
산업CompCert, ProofGeneralAWS Automated Reasoning
입문 난이도가파름가파르지만 Lean Game이 있음

Rocq가 죽었다는 뜻은 아니다 — 25년 누적된 산업 코드베이스는 어디 가지 않고, INRIA와 다수 학교가 여전히 강력히 지원한다.

5장 · Agda — 의존적 타입의 표본

Agda의 자리

Agda는 스웨덴 Chalmers 공과대학에서 시작된 순수 의존타입 함수형 언어다. Lean과 달리 "프로그래밍 언어로서의 정체성"이 더 강하다 — 즉 모든 함수는 종료해야 하고(totality check), 타입과 값의 구분이 거의 없다.

Agda의 표기 — 유니코드 천국

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero  + n = n
suc m + n = suc (m + n)

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm zero    n = sym (+-identity n)
+-comm (suc m) n = trans (cong suc (+-comm m n)) (sym (+-suc n m))

ℕ, ≡, ∀, → 모두 유니코드. 입력은 Emacs/VS Code의 Agda 모드가 \to, \equiv, \forall을 변환해 준다.

Agda의 강점

  • 타입과 값이 완전히 동일 — Lean보다 한 단계 더 순수
  • Cubical Agda — Homotopy Type Theory의 표준 구현
  • PLFA(Programming Language Foundations in Agda) — 학습 자료의 최고봉

Agda의 약점

  • 큰 표준 라이브러리가 없음(agda/stdlib이 있지만 mathlib에 비할 바 못 됨)
  • 산업 채택 거의 없음
  • 자동화(tactic)가 매우 약함 — 거의 수동 증명

2026년에 Agda를 배워야 하나

목적이 타입 이론 학습, HoTT 연구, PL 연구라면 그렇다. 산업 검증이나 큰 수학 라이브러리가 목적이라면 Lean 4가 낫다.

6장 · Idris 2 — Edwin Brady의 실용 의존타입

Idris 2의 정체성

Idris는 영국 St Andrews의 Edwin Brady가 만든 의존타입 함수형 언어다. Idris 1(2011)이 Haskell로 작성된 학술 프로토타입이었다면, Idris 2(2020~)는 Idris 자체로 다시 작성한 self-hosting 버전이고, 결정적으로 Quantitative Type Theory(QTT, Bob Atkey)를 채택했다.

Idris 2의 핵심 — Quantitative Types

data List : (a : Type) -> Type where
  Nil  : List a
  (::) : a -> List a -> List a

length : List a -> Nat
length [] = 0
length (_ :: xs) = 1 + length xs

-- 컴파일 타임에만 존재하는 인덱스 (0 quantity)
data Vect : Nat -> Type -> Type where
  Nil  : Vect 0 a
  (::) : a -> Vect n a -> Vect (S n) a

QTT는 각 인자에 0 / 1 / many 수량을 부여한다. 0은 컴파일 타임에만, 1은 정확히 한 번, many는 평범한 변수. 이걸로 의존타입과 선형타입을 동시에 다룬다.

Idris 2가 노리는 자리

Idris는 "프로그래밍을 위한 의존타입"을 가장 직설적으로 노린다. Lean이 수학, Agda가 PL 이론에 가까운 반면, Idris는 실제 소프트웨어 개발을 의식한다.

7장 · Isabelle/HOL — seL4를 증명한 도구

Isabelle의 정체성

Isabelle은 영국 Cambridge의 Larry Paulson과 독일 TUM의 Tobias Nipkow가 1986년부터 개발해온 고전 HOL(High-Order Logic) 기반 증명 보조기다. Lean/Coq/Agda가 constructive logic + 의존타입을 쓰는 반면, Isabelle/HOL은 고전 논리 + 단순타입을 쓴다.

Isabelle의 강점 — 자동화

Isabelle은 자동화가 매우 강력하다.

  • auto — 가장 강한 일반 자동 증명
  • metis — first-order ATP backend
  • sledgehammer — 외부 SMT/ATP(Z3, CVC4, E, Vampire 등)에 목표를 던지고 그들이 찾은 증명을 Isabelle 안에서 재구성
theorem add_comm: "(a::nat) + b = b + a"
  by (induct a) auto

한 줄. Lean이라면 simp나 omega를 호출하거나, 더 길게 induction을 풀어 쓴다. Isabelle은 "자동화 우선" 철학이다.

Isabelle의 대표 업적

  • seL4 마이크로커널 — NICTA(현 CSIRO Data61)와 UNSW가 약 200,000 LoC의 Isabelle 증명으로 9,000 LoC의 C 커널의 기능적 정확성, 무결성, 비밀성을 증명. 사람이 작성한 OS 코드 중 가장 강하게 검증된 코드.
  • Archive of Formal Proofs (AFP) — Isabelle 증명의 큐레이트된 저장소. 2026년 기준 700+ 항목.

2026년 Isabelle의 자리

산업 검증과 OS 보안에 가장 깊이 들어가 있는 도구. mathlib같은 수학 라이브러리는 적지만 자동화의 깊이는 압도적이다. seL4를 만진다면 사실상 Isabelle이 강제된다.

8장 · F* (FStar, Microsoft) — HACL* 암호 검증

F*의 정체성

F*(영어로 "FStar")는 Microsoft Research가 만든 의존타입 + SMT 자동화 + ML계 문법의 증명 지향 프로그래밍 언어다. 의존타입 측면에서는 Coq/Lean과 같은 계통이지만, Z3 SMT 솔버를 첫 번째 시민으로 가져와 일상적인 증명 책임의 상당 부분을 자동화한다.

짧은 F* 예시

val sorted_insert: x:int -> l:list int{sorted l}
  -> Tot (l':list int{sorted l' /\ Set.equal (set_of (x::l)) (set_of l')})
let rec sorted_insert x = function
  | [] -> [x]
  | y :: tl -> if x <= y then x :: y :: tl
               else y :: sorted_insert x tl

타입 안에 직접 사양(sorted l, Set.equal …)을 박는다. F*는 이걸 Z3에 던져 자동으로 풀려고 시도하고, 풀리지 않으면 사용자가 보조정리를 보강한다.

HACL* — 실제로 들어간 검증된 암호

F*의 가장 유명한 산업 사례는 HACL* — Curve25519, Poly1305, ChaCha20, SHA-2, HKDF, AES-GCM 등 표준 암호 알고리즘을 F*로 검증하고 C로 추출(extract)한 라이브러리다. 이 코드는:

  • Firefox의 NSS 라이브러리(서명, TLS)에 들어감
  • Linux 커널의 WireGuard VPN에 들어감
  • Windows / Azure의 일부 TLS 처리에 사용됨

즉 당신이 오늘 HTTPS를 쓸 때, F*로 검증된 코드가 그 어딘가에서 돌고 있을 가능성이 매우 높다.

EverCrypt / EverParse / Project Everest

HACL*는 더 큰 우산인 Project Everest 아래에 있다. EverCrypt(다중 알고리즘 디스패치), EverParse(검증된 메시지 파서) 등이 함께 묶여 있다. project-everest.github.io에 정리되어 있다.

F* vs Lean

항목F*Lean 4
자동화Z3 첫 번째 시민tactic + SMT는 별도
추출C, OCaml, .NET, JSC, IR (작업 중)
산업HACL*, Project Everestmathlib, AWS
수학 라이브러리적음거대(mathlib)

9장 · Liquid Haskell — refinement types

Liquid Haskell의 정체성

Liquid Haskell은 UCSD의 Ranjit Jhala 그룹이 만든 Haskell용 refinement type 시스템이다. 새로운 언어를 배우지 않고, 평범한 Haskell 코드에 사양 주석을 달면 SMT 솔버(주로 Z3)가 검증한다.

짧은 예시

{-@ type Pos = {v:Int | v > 0} @-}

{-@ divide :: Int -> Pos -> Int @-}
divide :: Int -> Int -> Int
divide x y = x `div` y

{-@ measure size @-}
size :: [a] -> Int
size []     = 0
size (_:xs) = 1 + size xs

{-@ type NonEmpty a = {v:[a] | size v > 0} @-}

{-@ head :: NonEmpty a -> a @-}
head :: [a] -> a
head (x:_) = x

{-@ ... @-} 안의 주석이 refinement spec이다. 컴파일러는 평범한 Haskell이지만, liquid 도구가 SMT로 사양을 검증한다.

강점과 약점

  • 강점: 의존타입 언어를 배우지 않고도 Haskell 코드를 검증할 수 있다. 진입장벽이 낮다.
  • 약점: Haskell 안에 갇혀 있다. 일반 정리 증명에는 못 쓴다. Z3에 못 풀리는 사양은 거기서 막힌다.

진짜 "산업의 검증된 Haskell"을 노린다면 Liquid Haskell이 현실적 첫 선택이다.

10장 · AI 보조 — DeepMind AlphaProof (IMO 2024 은메달)

AlphaProof란 무엇이었나

2024년 7월, DeepMind는 AlphaProof와 AlphaGeometry 2가 IMO 2024(국제수학올림피아드) 6문제 중 4문제(28/42점)를 풀어 은메달 점수를 받았다고 발표했다. 4문제 모두 정답에 도달하는 데 며칠씩 걸렸지만(인간 참가자는 시험 시간 안에 풀어야 함), 가장 어려운 P6(combinatorics)를 포함해 4개를 정답으로 풀어낸 것은 큰 사건이었다.

핵심 구조:

  1. 자연어 IMO 문제 → Lean 4 정리로 자동 번역 (auto-formalizer)
  2. Lean 4 안에서 강화학습으로 증명 탐색(AlphaProof = AlphaZero + Lean)
  3. 기하 문제는 AlphaGeometry 2(2023년 AlphaGeometry의 후속)가 따로 처리

DeepMind가 공개한 Lean 증명 자체는 사람이 봐도 매우 비인간적이다 — 100% 형식화된 한 줄 한 줄.

2025~2026년 후속

  • 2025년 IMO에서도 비공식적으로 비슷한 성과를 냈음(여러 비공식 보고)
  • DeepMind는 AlphaProof + LLM 페어 작업을 계속함
  • Lean 4와의 결합이 점점 깊어짐

의의

LLM이 자연어 풀이를 적당히 생성하던 시절을 지나, 형식적으로 검증된 풀이를 생성하는 시대로 들어갔다. 정답 여부를 컴파일러가 즉시 판정해 준다 — hallucination이 원리적으로 차단된다.

11장 · Anthropic + AIMO ($5M 상금)

AI Mathematical Olympiad (AIMO)

AIMO는 XTX Markets가 후원하는 $10M 규모의 AI 수학 올림피아드 챌린지다. 그 중 Grand Prize $5M은 IMO 수준의 문제 50개 중 일정 정확도 이상을 달성하는 AI 모델에 주어진다. (참고: AIMO 공식 사이트 aimoprize.com)

2024~2025년에 진행된 Progress Prize 라운드들에서 NuminaMath 등 여러 오픈소스 모델이 빠르게 발전했다. 2026년 현재 Grand Prize는 아직 수여되지 않았지만(공개적으로), 격차가 줄어들고 있다는 관측이 다수다.

Anthropic의 합류

Anthropic은 2024년 후반부터 수학 추론과 Lean 형식화를 Claude 모델의 명시적 평가 항목에 포함시켰다. 공개된 Claude의 수학 능력 기술 보고들에 따르면:

  • Claude는 자연어 수학 풀이를 생성하고, Lean으로 형식화할 때 점점 더 적은 사람 개입으로 끝낸다
  • Lean InfoView를 Claude가 컨텍스트로 받아 한 단계씩 tactic을 제안하는 워크플로가 mathlib 커뮤니티에 점점 자리잡고 있다 (예: Lean Copilot 프로젝트)
  • mathlib에 LLM 보조로 작성된 PR이 2025~2026년에 늘어났다

LeanDojo / LeanCopilot / ntp

학계에서도 비슷한 흐름이 있다.

  • LeanDojo (CMU) — Lean 환경을 LLM이 다룰 수 있게 만든 RL/툴 환경
  • LeanCopilot — Lean 안에서 직접 LLM tactic 제안
  • ntp-toolkit — Next-tactic prediction 표준 평가

이 도구들이 점점 합쳐져 "AI 보조 형식화"가 mathlib 일상이 되었다.

12장 · Terence Tao + Lean — 일류 수학자의 합류

Tao가 Lean을 만지기 시작한 계기

Terence Tao(UCLA, 필즈상 2006)는 한 세대 최고의 분석학자다. 그는 2023년부터 자기 블로그 terrytao.wordpress.com에서 Lean으로 형식화한 결과들을 정기적으로 공유한다.

대표 사건:

  1. 2023.11 — PFR Project — Tim Gowers, Ben Green, Freddie Manners와 공동 증명한 Polynomial Freiman-Ruzsa conjecture를 Lean으로 형식화. 약 3주에 20+명의 협업자가 완성. Tao는 이걸 "blueprint workflow"의 모범으로 제시.
  2. 2024 — Magma 추측 분류 프로젝트 — 4,694개의 magma equation을 Lean으로 계통적으로 분류. 수학적 문제를 Lean blueprint로 잘게 쪼개 분산 협업으로 해결한 사례.
  3. 2025~2026 — Tao는 자기의 새 논문 일부를 처음부터 Lean으로 작성, GitHub Copilot/Claude 보조 받음을 공개.

Tao가 강조하는 변화

Tao 본인이 여러 강연(예: IAS, Joint Mathematics Meetings)에서 강조한 메시지:

  • "10년 전 형식화는 1쪽 증명에 1년이 걸렸다. 지금은 1주일이고, 5년 안에 같은 날에 끝난다."
  • "검증된 라이브러리는 수학자의 단위 테스트다. 우리가 쓰는 결과가 진짜 옳다는 보증."
  • "AI는 형식화의 가장 지루한 부분을 가져간다. 수학자는 더 위로 올라간다."

Kevin Buzzard와 학부 교육

Imperial College London의 Kevin Buzzard는 학부 1학년에게 Natural Number Game이라는 브라우저 Lean 퍼즐을 시키며, "모든 수학과 학부생은 Lean을 배워야 한다"고 공개 주장한다. 이 흐름이 2026년에는 5~10개 일류 대학에서 학부 정규 과목으로 자리잡았다.

13장 · Z3 + CVC5 — 그 밑단의 SMT 솔버

SMT solver란

SMT(Satisfiability Modulo Theories) 솔버는 "이 1차 논리식이 어떤 모델에서 참이 되는지" 자동으로 푸는 엔진이다. 정리 증명기가 "사람이 한 줄씩 쓰는" 도구라면, SMT 솔버는 "수식 한 덩어리를 통째로 던지면 자동으로 답하는" 도구다.

Z3

Z3는 Microsoft Research(2007~, Leonardo de Moura가 핵심 저자)가 만든 가장 영향력 있는 SMT 솔버다. 무료/오픈소스(MIT). 대표 사례:

  • F* / Liquid Haskell의 백엔드
  • Microsoft Driver Verifier
  • AWS Zelkova (S3 정책 검증)
  • 컴파일러 검증, 모델 체커, 정적 분석기의 표준 백엔드

CVC5

CVC5(Stanford + 다수 기관, CVC4의 후속, 2022~)는 Z3의 가장 강한 경쟁자다. 일부 도메인(특히 string, datatype)에서 Z3보다 빠르다. CASC/SMT-COMP 같은 대회에서 Z3와 CVC5가 1, 2위를 다툰다.

짧은 예시 — SMT-LIB

(set-logic QF_LIA)
(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (> y 0))
(assert (= (+ x y) 10))
(check-sat)
(get-model)

QF_LIA는 "quantifier-free linear integer arithmetic". 두 솔버 모두 같은 표준 입력을 받는다.

2026년의 자리

  • F*, Dafny(MS), Why3(INRIA) 등 검증 언어 백엔드
  • Sledgehammer(Isabelle)가 외부로 던지는 솔버 후보 중 하나
  • AWS Zelkova / Tiros — IAM 정책의 안전성을 SMT로 검증해 실시간 경고
  • Java PathFinder, KLEE — 심볼릭 실행에서 path constraint solver

SMT 솔버는 정리 증명기 사용자가 자주 의식하지 않는 "엔진룸"이지만, 거의 모든 자동화의 뒤에 둘 중 하나가 돌고 있다.

14장 · 형식 검증 사례 — seL4 / CompCert / IronFleet / KLEE

seL4 — 검증된 마이크로커널

2009년 NICTA(현 CSIRO Data61)와 UNSW가 발표한 seL4는 약 9,000 LoC의 C 마이크로커널을, 200,000+ LoC의 Isabelle/HOL 증명으로 검증한 사상 최초의 본격 OS 커널이다. 증명 내용:

  • 기능적 정확성 — C 코드가 abstract spec과 행동이 정확히 같다
  • 무결성 — 권한 없는 접근이 불가능하다
  • 비밀성 — 정보 흐름 제약이 보존된다

이 커널은 군용 항공, 위성, 일부 자율주행 시스템에서 실제로 돌고 있다. seL4 Foundation이 오픈소스로 유지한다.

CompCert — 검증된 C 컴파일러

Xavier Leroy(INRIA, 콜레주 드 프랑스)의 CompCert는 Coq(현 Rocq)로 작성·검증된 C 컴파일러다. C 표준의 부분집합(거의 전체)을 받아 PowerPC/ARM/x86 어셈블리로 컴파일하면서, "원본 C 의미 == 출력 어셈블리 의미"를 Rocq로 증명한다.

CSmith fuzzing 연구가 GCC/Clang에서는 수십 개의 컴파일러 버그를 찾아낸 반면, CompCert에서는 단 하나의 컴파일러 버그도 찾지 못했다(다만 spec gap 일부 발견). Airbus 등 항공 산업에서 실제 사용된다.

IronFleet / IronClad

Microsoft Research의 IronFleet는 분산시스템(Paxos, lock service)을 Dafny(Z3 백엔드)로 종단 검증했다. 비잔틴이 아닌 환경에서 안전성/활성성/선형화 가능성을 동시에 증명한 첫 본격 사례.

KLEE — 심볼릭 실행

KLEE는 LLVM IR 위에서 동작하는 심볼릭 실행 엔진이다. 검증과는 결이 다르지만(부분 경로 탐색) 실제 코드의 버그 발견에 매우 효과적이다. coreutils, BusyBox 등에서 수많은 버그를 발견했다.

정리하면

도구검증 대상백엔드
seL4OS 커널Isabelle/HOL
CompCertC 컴파일러Rocq
IronFleet분산 시스템Dafny + Z3
HACL* / EverCrypt암호 라이브러리F* + Z3
KLEE일반 LLVMSMT (Z3/STP)
AWS ZelkovaIAM 정책Z3

15장 · 한국 / 일본 — KAIST · ETRI · 京都大学 · 東京大学 · AIST

한국

  • KAIST 전산학부 PL/Verification 그룹 — Software Reliability Lab(SRL, psl.kaist.ac.kr) 등에서 Coq/Rocq 기반 형식 검증 연구. 곽재두 교수 그룹은 CompCert 확장 작업으로 알려짐.
  • POSTECH, 서울대 PL 연구실 — 함수형/타입 이론/검증 연구가 꾸준함.
  • ETRI 형식 검증 그룹 — 정부 과제로 OS/보안 검증 연구.
  • 학부 강의로 Coq/Lean을 정규 도입한 사례는 아직 적지만 2024~2026년 사이 늘고 있다.

일본

  • 京都大学 木下研究室 / 五十嵐研究室 — PL/타입 이론에서 일본 전통 강자. Coq 활용.
  • 東京大学 蓮尾研 / 小林研 — formal verification, 모델 체킹.
  • AIST(産業技術総合研究所) Cyber Physical Security Research Center — Z3/CVC5/Isabelle 활용 보안 검증.
  • NII(国立情報学研究所) — 수리논리/타입 이론 연구.
  • オートマトン理論과 정리 증명을 묶는 ALGI 같은 학회 흐름이 살아있다.

한국어 / 일본어 자료

  • 한국어: 한경수 교수의 KAIST CS220 자료, 일부 블로그(hyperpolyglot, 김재선 블로그 등). 절대량은 적다.
  • 일본어: qnighy(Microsoft, Rust/Coq), mzp 등 일본 Coq/Lean 사용자 블로그. 한국보다 활성화되어 있다.

두 나라 모두 영어 자료(mathlib zulip, Coq Discourse, FStar GitHub)로 진입하는 것이 사실상 표준이다.

16장 · 누가 정리 증명기를 배워야 하나

학부 수학생

Lean 4 + mathlib이 단연 1순위다. Imperial College의 Natural Number Game (브라우저에서 바로 플레이 가능)을 1주일 해보고, Mathematics in Lean을 한 챕터씩 따라가면 6개월 안에 자기 학부 과목의 정리들을 형식화할 수 있다.

대학원 수학자 / 연구자

목표가 자기 논문 형식화 + mathlib 기여라면 Lean. Tao를 보라. 단, 자기 분야가 이미 Coq/Rocq나 Isabelle에 두텁게 있다면(예: 정수론 일부, 위상 일부) 그 흐름을 따르는 것이 효율적.

PL 연구자 / 컴파일러 / 타입 시스템

Rocq (Coq) 또는 Agda. CompCert, Iris, software foundations의 흐름이 여기에 있다. Agda는 HoTT/Cubical에 관심 있다면 필수.

보안 엔지니어 / 암호 엔지니어

F* 또는 Isabelle/HOL. HACL*/EverCrypt에 들어가고 싶다면 F*. OS/마이크로커널 보안이라면 seL4 → Isabelle 경로.

백엔드 / 일반 개발자

Dafny, Liquid Haskell, 또는 TLA+(Lamport)로 시작. 본격 정리 증명기보다 entry barrier가 낮고, 코드/스펙에 바로 적용된다.

"그냥 궁금해서"인 사람

Lean Game Server의 게임들로 시작하라. Natural Number Game, Set Theory Game, Cantor's World 등이 브라우저에서 돈다. 한 시간이면 첫 증명을 깬다.

17장 · 마무리 — 형식화는 더 이상 미래의 일이 아니다

2026년의 풍경을 정리하면:

  1. Lean 4 + mathlib가 수학 형식화의 사실상 표준이 되었다. 100만 정리, 일류 수학자의 일상 도구.
  2. **Rocq (구 Coq)**는 산업 검증(CompCert, seL4 보조)을 굳건히 유지하며 25년 역사를 잇는다.
  3. Agda / Idris 2는 타입 이론·PL 연구의 도구로 자리를 지킨다.
  4. Isabelle/HOL + sledgehammer는 자동화의 깊이로 seL4 같은 산업 검증을 가능케 한다.
  5. F* + Z3 + HACL*는 당신이 오늘 쓰는 HTTPS 안에 이미 있다.
  6. DeepMind AlphaProof, Anthropic AIMO가 AI 보조 형식화 시대를 열었다. Lean과 LLM이 일상적으로 페어 프로그래밍한다.
  7. seL4, CompCert, IronFleet가 "형식 검증은 학계 이야기"라는 변명을 박살냈다. 실제 시스템에서 돌아간다.

10년 전 "곧 형식화가 표준이 될 것"이라 말했다면 비웃음을 샀을 것이다. 2026년에 같은 말을 하면 이미 그렇게 되어 있다고 답해야 한다.

수학자에게: Lean 4를 시작하라. Tao가 이미 했다. 보안 엔지니어에게: 당신의 다음 암호 코드는 F* 검증을 거쳐야 한다. 시스템 엔지니어에게: seL4 위에서 컴포넌트를 짜는 시대가 곧 온다. 호기심 있는 모두에게: Lean Game Server를 한 시간만 해보라.

증명은 더 이상 종이 위의 일이 아니다.

참고 / References

Discuss on Twitter • View on GitHub