AI가 Formal Verification을 주류로 만들 것이다

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

관련 논문

• LLM이 TLA+로 실제 시스템을 제대로 모델링할 수 있을까? — SysMoBench 벤치마크

  LLM이 TLA+ 명세를 작성할 때 문법은 잘 통과하지만 실제 시스템과의 동작 일치도(conformance)는 46% 수준에 그친다는 걸 체계적으로 검증한 벤치마크 연구로, AI 기반 형식 검증의 현실적 한계를 보여준다.

• Natural Language Autoencoders: Claude의 내부 활성화를 자연어 텍스트로 변환하는 기법

  Anthropic이 LLM 내부의 숫자 벡터(활성화값)를 직접 읽을 수 있는 자연어로 변환하는 NLA 기법을 공개했다. AI가 실제로 무슨 생각을 하는지 해석하는 interpretability 연구의 새로운 진전이다.

• ProgramBench: LLM이 프로그램을 처음부터 다시 만들 수 있을까?

  LLM이 FFmpeg, SQLite, PHP 인터프리터 같은 실제 소프트웨어를 문서만 보고 처음부터 재구현할 수 있는지 측정하는 새 벤치마크로, 최고 모델도 전체 태스크의 3%만 95% 이상 통과하는 수준에 그쳤다.

• MOSAIC-Bench:코딩 에이전트의 Compositional Vulnerability 유도 측정

  티켓 3장으로 쪼개면 Claude/GPT도 보안 취약점 코드를 53~86% 확률로 그냥 짜준다.

• LLM의 거절(Refusal) 동작은 단 하나의 방향(Direction)으로 제어된다

  13개의 오픈소스 채팅 모델을 분석했더니, 모델이 유해한 요청을 거절하는 동작이 내부 활성화 공간에서 단 하나의 1차원 벡터 방향으로 인코딩되어 있었다. 이 방향을 제거하면 안전 파인튜닝이 사실상 무력화되므로, 현재 안전 학습 방식이 얼마나 취약한지 보여준다.

• LLM의 구조화된 출력(Structured Output)을 테스트하는 새 벤치마크 SOB 공개

  스키마 준수 여부만 보던 기존 벤치마크의 한계를 넘어, 실제 값의 정확도까지 7가지 지표로 평가하는 Structured Output Benchmark(SOB)가 공개됐다. 인보이스 파싱, 의료 기록 추출처럼 JSON 출력의 정확성이 중요한 프로덕션 시스템에서 어떤 모델을 써야 할지 판단하는 데 직접적으로 참고할 수 있다.

Related Resources

• https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html
• https://quint-lang.org/posts/llm_era
• https://leandojo.org/leandojo.html
• https://aristotle.harmonic.fun/