---
title: "AI가 형식 검증을 메인스트림으로 끌어올릴 것이라는 예측"
published: 2025-12-08T23:01:06.000Z
canonical: https://jeff.news/article/599
---
# AI가 형식 검증을 메인스트림으로 끌어올릴 것이라는 예측

Martin Kleppmann이 AI가 형식 검증(formal verification)을 주류로 만들 것이라 예측. LLM이 증명 스크립트 작성 비용을 급격히 낮추고, AI 생성 코드에 대한 검증 필요성이 이를 가속할 것이라는 논지.

## 형식 검증의 현주소: 비싸고 어려움

- 증명 보조 도구(Rocq, Isabelle, Lean, F*, Agda 등)는 오래전부터 존재했지만, 증명 작성에 박사급 전문 지식이 필요하고 작업량이 막대해서 산업계에서는 거의 쓰이지 않았음
- 대표적 사례로 seL4 마이크로커널은 C 코드 8,700줄을 검증하는 데 20인년이 소요되었고, Isabelle 증명 코드가 20만 줄 필요했음. 구현 코드 1줄당 증명 23줄, 반나절의 작업량이라는 뜻
- 경제적으로 보면, 대부분의 시스템에서 버그의 예상 비용이 형식 검증 비용보다 낮아서 굳이 할 이유가 없었음. 버그 비용을 개발자가 아닌 사용자가 부담하는 구조도 한몫함

## AI가 바꾸는 경제성

- LLM 기반 코딩 어시스턴트가 구현 코드뿐 아니라 증명 스크립트 작성에도 점점 능숙해지고 있음. 아직은 전문가가 가이드해야 하지만, 수년 내 완전 자동화가 가능할 것으로 예상됨
- 형식 검증 비용이 급격히 낮아지면 훨씬 더 많은 소프트웨어를 검증할 수 있게 됨
- 동시에 AI 생성 코드가 늘어나면서 형식 검증의 필요성도 커짐. 사람이 AI 코드를 리뷰하는 것보다 AI가 코드의 정확성을 수학적으로 증명해주는 편이 훨씬 나음

## LLM과 증명 체커의 궁합

- LLM이 증명 스크립트를 작성하는 건 사실 LLM의 최적 활용처 중 하나임. 환각(hallucination)이 일어나도 증명 체커가 잘못된 증명을 자동으로 거부하고 재시도하게 만들 수 있기 때문
- 증명 체커 자체가 소량의 검증된 코드로 이루어져 있어서, 잘못된 증명이 통과할 가능성은 사실상 없음

## 남은 과제와 전망

- 검증 자체가 자동화되면 도전 과제는 올바른 명세(specification) 작성으로 이동함. "증명된 속성이 정말 원하는 속성인가?"를 정의하는 데 여전히 전문성과 신중한 사고가 필요함
- 하지만 명세 작성은 증명 작성보다 훨씬 쉽고 빠르므로 큰 진전임. AI 에이전트가 자연어와 형식 언어 간 번역을 도울 가능성도 있음
- 궁극적으로는 원하는 속성을 선언적으로 명세하고, 구현과 증명은 바이브 코딩으로 돌리는 미래가 올 수 있음. 컴파일러가 생성한 머신 코드를 안 보듯이, AI가 생성한 코드도 안 봐도 되는 세상
- Kleppmann은 기술보다 문화 변화가 더 큰 장벽이 될 것이라고 봄. 형식 검증이 실용적이 되었다는 사실을 업계가 인식하는 것이 관건

## 핵심 포인트

- seL4 커널 8,700줄 검증에 20인년과 20만 줄의 증명 코드가 필요했음
- LLM이 증명 스크립트 작성에 점점 능숙해지는 중
- AI가 형식 검증 비용을 급격히 낮출 것
- AI 생성 코드야말로 형식 검증이 필요한 대상
- 증명 체커가 LLM 환각을 자동으로 걸러내므로 궁합이 좋음

## 인사이트

AI 코드 생성의 신뢰성 문제를 형식 검증으로 풀자는 발상이 신선함. 바이브 코딩의 다음 단계가 '검증된 바이브 코딩'이 될 수도