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은 기술보다 문화 변화가 더 큰 장벽이 될 것이라고 봄. 형식 검증이 실용적이 되었다는 사실을 업계가 인식하는 것이 관건