AI가 쓴 코드, Lean으로 기계 검증하는 시대 열린다

AI가 코드를 대신 작성하는 시대에 남는 병목은 생성이 아니라 검증이다. Lean 창시자이자 AWS 부사장 겸 Lean Focused Research Organization 수석 아키텍트인 레오 드 무라는 이 문제를 형식 검증으로 풀 수 있다고 본다. Lean은 프로그래밍 언어이면서 정리 증명기다. 코드를 작성하는 동시에 그 코드가 만족해야 할 성질을 선언하고, 기계가 확인하는 증명을 붙일 수 있다.

Lean의 신뢰 기반은 작은 커널이다. 방대한 도구와 라이브러리가 있어도 증명 검사 자체는 커널이 맡고, 증명은 데이터처럼 추출해 다른 검사기로도 확인할 수 있다. 드 무라에 따르면 현재 두 개의 검증된 검사기가 있고 세 번째도 준비 중이다. 이런 구조 덕분에 사람과 AI 사이의 신뢰 문제도 다룰 수 있다. 원하는 성질을 먼저 적고, AI에게 그 성질을 만족하는 코드와 Lean 증명을 함께 만들게 하는 식이다.

구체적인 사례로 김 모리슨이 zlib 압축 라이브러리를 Lean으로 옮긴 실험이 있다. 이식된 코드에는 압축한 뒤 해제하면 원본 데이터가 그대로 복원된다는 성질이 정리로 명시됐고, 압축 수준도 정리의 매개변수로 포함됐다. 데이터 손실이나 변형 없이 왕복이 보장된다는 뜻이다. 드 무라는 AI가 이런 코드 구현과 증명 작성을 함께 할 수 있는 수준에 왔다고 평가했다.

Rust 코드를 Lean으로 검증하는 길도 열려 있다. Aeneas는 Rust 프로그램을 Lean 모델로 바꿔 성질을 증명하는 도구로, 마이크로소프트 SymCrypt 팀이 암호 라이브러리 검증에 활용한다. 또한 AI가 어떤 언어로 작성된 코드든 읽고 Lean 모델을 만들어낼 수 있다. 수학 논문을 형식 언어로 옮기는 오토포멀라이제이션도 최근 프런티어 모델의 성능 향상으로 현실적인 작업이 됐다.

전통적인 테스트는 버그를 찾는 데 유용하지만 버그가 없음을 증명하지는 못한다. 형식 검증은 속성 기반 테스트의 한계를 넘어 '신뢰해 달라'는 요구를 기계적 증명으로 바꾼다. 드 무라는 AI 에이전트의 행동, 샌드박스, 보안 정책까지 검증 대상으로 확장되는 그림을 그린다. 소프트웨어 스택 전체를 검증된 구성요소로 쌓는 비전도 여기서 나온다.

개발자에게 이 흐름은 역할 변화를 뜻한다. 코드를 직접 짜는 일보다 원하는 성질과 명세를 정확히 적는 능력이 중요해진다. 물론 한계도 있다. 증명 검사기를 신뢰하더라도 요구사항 누락이나 모델과 실제 코드 사이의 간극은 남는다. AI가 만든 형식 모델이 원본 코드를 제대로 반영하는지 확인해야 하고, Mathlib 같은 대형 라이브러리를 확장하는 일은 여전히 규모의 문제다.