AI가 Formal Verification을 주류로 만들 것이다
AI will make formal verification go mainstream
TL;DR Highlight
Martin Kleppmann이 LLM 기반 코딩 어시스턴트가 수십 년간 학계에 머물던 형식 검증(formal verification)을 산업 현장의 주류 기술로 끌어낼 것이라고 예측한다. AI가 증명 스크립트 작성을 자동화하면 비용 문제가 해결되고, 동시에 AI 생성 코드의 신뢰성을 보장하는 도구로 형식 검증이 필요해지는 선순환 구조가 만들어진다는 주장이다.
Who Should Read
AI 코딩 에이전트를 실무에 도입했거나 도입을 검토 중인 시니어 개발자, 또는 암호화·운영체제·컴파일러처럼 높은 신뢰성이 요구되는 시스템을 개발하는 엔지니어.
Core Mechanics
- 형식 검증(formal verification)이란 코드가 명세(spec)를 항상 만족한다는 것을 수학적으로 증명하는 기법이다. Rocq(구 Coq), Isabelle, Lean, F*, Agda 같은 증명 보조 도구(proof assistant)가 수십 년째 존재했지만, seL4 마이크로커널 사례처럼 C 코드 8,700줄을 검증하는 데 20인년·Isabelle 코드 20만 줄이 필요할 정도로 비용이 막대해 연구 외 산업 현장에서는 거의 쓰이지 않았다.
- LLM이 증명 스크립트 작성에서 두각을 나타내고 있다. 현재는 전문가가 방향을 잡아줘야 하지만, 저자는 수년 내 완전 자동화가 가능하다고 본다. 그렇게 되면 형식 검증의 경제성이 근본적으로 바뀐다.
- 증명 스크립트 작성은 LLM에게 특히 적합한 작업이다. 환각(hallucination)이 발생해도 증명 체커가 틀린 증명을 즉시 거부하고 재시도를 강제하기 때문에, 코드 생성과 달리 오류가 자동으로 걸러진다. 증명 체커 자체는 소량의 검증된 코드로 구성되어 있어 우회가 사실상 불가능하다.
- AI가 형식 검증을 더 필요하게 만드는 역설이 있다. AI 생성 코드를 인간이 일일이 리뷰하는 대신, AI가 코드와 함께 그 코드의 정확성 증명을 제출하면 리뷰 없이도 신뢰할 수 있다. 저자는 이를 컴파일러 생성 기계어를 굳이 보지 않는 것과 같은 수준의 신뢰라고 비유한다.
- 형식 검증이 자동화되면 남은 과제는 명세(specification) 작성이다. 증명된 속성이 실제로 원하던 속성인지 확인하는 일이다. 명세 작성은 증명 작성보다 훨씬 쉽고 빠르기 때문에 병목이 이동하는 것이지 사라지는 게 아니다.
- AI 에이전트가 자연어와 형식 언어 사이를 번역하는 방식으로 명세 작성도 보조할 수 있다고 저자는 예상한다. 번역 과정에서 뉘앙스가 손실될 위험은 있지만 관리 가능한 수준이라고 본다.
- 궁극적인 비전은 '바이브 코딩(vibe coding, 자연어로 대략 설명하면 AI가 코드를 짜는 방식)'과 형식 검증의 결합이다. 개발자가 원하는 속성을 고수준으로 선언하면, AI가 구현 코드와 그 코드의 정확성 증명을 함께 생성하는 형태다.
Evidence
- 형식 검증이 일상적 프로그래밍 문제에는 맞지 않는다는 반론이 많았다. UI의 혼란스러운 문구, 외부 API 변경, 고객이 원하는 것을 모르는 상황, OS·DB·네트워크가 얽힌 복잡한 시스템 등은 수학적으로 명세를 정의하기 어렵다는 지적이다. 댓글들은 형식 검증이 빛을 발하는 영역을 암호화 구현이나 컴파일러 최적화처럼 구현이 명세보다 훨씬 복잡한 저수준 라이브러리로 한정했다.
- 실제로 Lean 4를 실무에 쓰기 시작했다는 경험담이 큰 호응을 얻었다. 박사 과정에서 Coq로 6개월 걸리던 작업이 LLM 도움으로 수 시간~수 일로 줄었다는 증언이다. 이 댓글 작성자는 LLM을 증명 내부의 오라클로 사용하는 아이디어(검증되지 않은 코드가 체크 가능한 증명서를 만들고, LLM이 추측한 불변식도 체커를 통과해야 유효하다는 구조)를 실험 중이라고 공유했다.
- 문화와 인센티브 문제가 기술적 난이도보다 더 큰 장벽이라는 의견이 공감을 받았다. 테스트 스위트 하나 제대로 유지 못하는 조직이 TLA+/Dafny/Lean으로 정밀한 명세를 작성하고 이를 블로킹 아티팩트로 다루길 기대하는 건 현실적이지 않다는 것이다. 대신 property-based test, contract, refinement type처럼 'CI의 체크박스처럼 보이는' 형태로 도입되면 가능성이 있다는 현실적 대안이 제시됐다.
- 폭포수(waterfall) 방식의 퇴장이 형식 검증이 외면받은 진짜 이유라는 역사적 지적도 있었다. 긴 명세 문서를 먼저 쓰는 방식은 애자일이 등장하면서 버려졌고, 그 이유는 명세 작성자가 사용자 요구를 오해하거나 사용자 스스로 원하는 것을 몰랐기 때문이었다. AI가 증명 비용을 줄여줘도 이 근본 문제는 해결되지 않는다는 비판이다.
- 형식 검증 도구가 AI 학습에서 핵심 역할을 한다는 ML 연구자 관점의 댓글도 주목받았다. Lean 같은 시스템이 보상 해킹(reward hacking) 없는 명확한 보상 신호와 '그라운딩된(grounded)' 환경을 제공하기 때문에, 강화학습 기반 AI 개선에 이상적이라는 주장이다. LeanDojo 프로젝트가 예시로 언급됐다.
How to Apply
- 암호화 라이브러리, 파서, 압축 코덱처럼 명세가 명확한 저수준 라이브러리를 작성 중이라면, Claude나 GPT에게 Lean 4로 핵심 함수의 속성(예: 역함수 관계, 단조성)을 증명하는 스크립트를 생성하게 해보면 된다. 증명이 틀려도 체커가 즉시 알려주므로 할루시네이션 위험이 낮다.
- AI 코딩 에이전트(Claude Code, Codex CLI 등)를 쓰고 있다면, 에이전트가 코드를 직접 실행·검증할 수 있는 환경 구축이 먼저다. Python이면 바로 실행, 프론트엔드라면 Playwright 연동, 그 위에 property-based test(Hypothesis, fast-check)를 붙이는 순서로 검증 레이어를 쌓으면 에이전트 품질이 눈에 띄게 좋아진다.
- 분산 합의 엔진, 상태 머신 같은 복잡한 프로토콜 변경을 앞두고 있다면, Quint 형식 명세를 LLM 프롬프트 중간에 끼워 넣는 실험적 워크플로(댓글에서 언급된 quint-lang.org 사례)를 참고할 수 있다. 명세가 프롬프트의 앵커 역할을 해서 AI가 범위를 벗어나는 구현을 줄이는 효과가 있다.
- 지금 당장 Lean을 도입하기 어렵다면, 'CI 체크박스'처럼 느껴지는 방식부터 시작하면 된다. pytest-hypothesis(Python), fast-check(TypeScript) 같은 property-based test 도구로 핵심 비즈니스 로직의 불변식을 LLM에게 추출하게 하고 CI에 추가하면, 형식 검증의 철학을 낮은 비용으로 적용할 수 있다.
Terminology
formal verification코드가 명세를 100% 만족한다는 것을 수학적 증명으로 보장하는 기법. '테스트'는 특정 입력에서 동작을 확인하지만, 형식 검증은 모든 가능한 입력에 대해 보장한다.
proof assistant사람이 수학 증명을 작성할 때 각 단계가 논리적으로 올바른지 검사해주는 소프트웨어. Lean, Rocq(구 Coq), Isabelle 등이 대표적이다.
proof script증명 보조 도구가 이해할 수 있는 형식 언어로 작성된 증명 코드. 구현 코드와 별개로 작성되며, 코드가 명세를 만족하는 이유를 단계별로 서술한다.
specification (명세)소프트웨어가 만족해야 할 속성을 형식 언어로 정의한 것. 예: '이 함수는 항상 정렬된 배열을 반환한다'. 증명의 목표가 되는 대상이다.
property-based testing구체적인 테스트 케이스 대신 '이 함수는 항상 X라는 성질을 만족해야 한다'는 속성을 정의하면, 도구가 무작위로 수천 가지 입력을 생성해 반례를 찾는 테스트 방식이다.
reward hackingAI가 보상 함수의 허점을 이용해 실제 목표와 다른 방식으로 높은 점수를 얻는 현상. 예: 테스트를 통과하도록 테스트 자체를 수정하는 AI.