수학 정리나 소프트웨어의 정확성을 기계적으로 보증하려는 증명 보조 도구(proof assistant)에서 가장 민감한 부분은 커널, 즉 증명 검사기다. 커널이 잘못된 증명을 받아들이면 그 위에 쌓인 모든 보증이 무너지기 때문이다. Lean의 창시자 Leonardo de Moura가 공개한 글은 바로 이 커널의 신뢰성을 강화하기 위한 일련의 작업을 정리하고 있다. 배경에는 AI 에이전트가 소프트웨어의 취약점을 매우 효과적으로 찾아낸다는 현실이 있다. Lean 커널도 예외가 아니어서, 8월 1일과 8월 24일 두 차례의 사후분석(postmortem)이 공개된 바 있다. 커널이 공격 대상이 될 수 있다는 점이 드러난 이상, 하나의 구현을 신뢰하는 구조 자체를 재검토할 필요가 생긴 것이다.
재검사를 일상 작업으로
Lean v4.35.0에는 lake check 명령이 추가됐다. 이 명령은 사용자의 개발 결과물을 내보낸 뒤 leanchecker, 즉 주변 기능을 모두 걷어낸 공식 Lean 커널로 다시 검사한다. 전체 과정은 샌드박스 안에서 실행되며, 필요하다면 lake check --inadvisably-no-sandbox로 샌드박스를 끌 수 있다. 명령 이름에 '권장하지 않음(inadvisably)'을 박아 넣은 것에서 설계 의도가 드러난다. 나아가 Lean에는 nanoda, lean4lean, con-leche, con-ron 네 개의 추가 커널이 함께 배포되며, lake check --paranoid를 쓰면 이 모두로 한 번에 재검사할 수 있다. 이 모드에서는 강화된 메모리 할당기로 빌드한 공식 커널 변종도 함께 돌아가는데, 메모리 손상을 조용히 틀린 답으로 흘려보내는 대신 검사된 중단(checked abort)으로 바꿔준다.
일관성이 증명된 커널, con-leche
이번 발표에서 가장 눈에 띄는 것은 con-leche다. Lean으로 작성되고 일관성(consistency)이 증명된 최초의 Lean 커널로, Lean FRO의 Joachim Breitner가 면밀히 감독하는 가운데 Claude(Fable, Opus)가 구현하고 그 일관성을 증명했다고 한다. 여기서 말하는 '일관성'은 con-leche가 받아들이는 모든 환경이 집합론 안에서 모델을 가진다는 뜻이며, 이는 Mario Carneiro가 제시한 Lean 타입 이론의 모델을 따른다. 증명 자체는 공식 Lean 커널로 검사되고, 모델에 사용된 집합론의 일관성을 전제로 한다. 이 접근은 '커널 구현의 프로그래밍 실수'라는 버그 부류 하나를 통째로 제거하는데, 성능 손해도 없다. 전체 Mathlib 내보내기 기준으로 con-leche는 공식 커널 대비 0.69배의 명령어만 실행하며, 여덟 스레드로 약 100초 만에 라이브러리 전체를 검사한다.
다만 con-leche도 완벽하지는 않다. 이를 빌드하는 데 쓰인 컴파일러와 런타임에 버그가 있을 수 있기 때문이다. 이 위험을 줄이기 위해 Joachim은 AI를 이용해 con-leche를 Rust로 번역하고, Aeneas로 그 Rust 버전이 con-leche의 검사 알고리즘을 정제(refine)함을 증명했다. Aeneas는 Lean을 이용해 Rust 코드를 검증하는 도구이며, 이렇게 만들어진 커널이 con-ron이다. 핵심 논리는 이렇다. con-leche에 형식적 일관성 증명이 있는 이상, 남아 있는 건전성(soundness) 버그는 대개 Lean의 컴파일러나 런타임(빅넘 라이브러리 포함)에 있을 가능성이 높다. 같은 버그가 Rust 컴파일러와 런타임에도 똑같이 존재할 확률은 매우 낮으므로, 두 커널로 함께 검사하면 이 부류의 버그에 대해 높은 수준의 방어를 얻게 된다.
다중 커널 전략의 의미
이 전략의 실무적 의미는 '단일 신뢰 지점'을 흩뜨리는 데 있다. 하나의 커널 구현을 믿는 대신, 서로 다른 언어·구현·검증 경로를 가진 여러 커널이 같은 증명에 동의하도록 요구함으로써, 어느 한 구현의 결함이 결과 전체를 오염시킬 확률을 낮춘다. de Moura는 앞으로 몇 달 안에 lean4lean의 검증도 완료될 것으로 보며, 그러면 배포판에 검증된 커널이 셋 생긴다고 밝혔다. lean4lean은 공식 C++ 커널 구현을 매우 가깝게 따른다는 점에서 의미가 있다. 한편 Arthur Adjedj는 커널 개편 계획(이슈 #14977)을 진행하며 여러 PR을 제출했고, Joachim은 이를 검토하면서 con-leche가 동일한 변경을 반영하도록, 그리고 개편 과정에서 증명에 새 구멍이 생기지 않도록 증명을 함께 보정하고 있다. 더 단순한 커널을 만들어 명세 검증 자체를 간소화하려는 작업도 병행 중이다.
남은 과제는 규모
물론 과제는 많다. 더 쓰기 편한 lake check, 사용자가 선호하는 커널을 연결할 수 있는 구조, Lean Kernel Arena에 쌓인 효율적인 커널들의 손쉬운 활용, 그리고 컴파일러 일부의 검증까지 과제 목록에 올라 있다. 그러나 가장 현실적인 벽은 규모다. Anthropic의 FLT는 1,300만 줄이 넘고 Mathlib은 250만 줄, Tau Ceti는 이미 300만 줄을 넘어 빠르게 커지고 있으며, General Courtade–Kumar 정리 저장소는 5,000만 줄을 웃돈다. 심지어 10억 줄 규모의 수학 라이브러리 제안까지 커뮤니티에서 나오는 상황에서, 지금의 외부 커널 재검사 방식은 이런 덩치를 감당하지 못한다. 이진 내보내기 형식과 외부 검사기의 증분(incremental) 검사가 필요하다는 것이 de Moura의 진단이다. 당장 할 수 있는 일은 명확하다. 자신의 프로젝트에서 lake check --paranoid를 돌려보고, 커널들이 어떤 증명을 두고 서로 다른 판정을 내린다면 contact@lean-fro.org로 알리는 것이다. 바로 그 불일치가 숨은 버그를 드러내는 신호이기 때문이다.