Lean 커널 건전성 버그 #14576 사후 분석
원제: Postmortem for Kernel Soundness Bug #14576
왜 중요한가
정리 증명 보조기의 핵심인 커널 건전성 버그 발견·수정 과정은 형식 검증 생태계의 신뢰성과 다중 독립 검사기 체계의 중요성을 재조명한다.
2026년 7월 25일, Ramana Kumar가 AI 지원으로 Collatz 추측의 'sorry-free 반증'을 공개했다. 이는 Lean 커널의 중첩 귀납 타입 처리 버그를 악용한 것으로, 7월 28일 Kiran Gopinathan이 이슈 #14576을 제기했으며, 보고 1시간 만에 수정 패치 #14577이 배포됐다.
Lean 커널 개발자 Leonardo de Moura가 2026년 8월 1일 건전성 버그 #14576에 대한 공식 사후 분석을 공개했다.
**버그 내용**: 커널이 파라미터 Ds를 가진 귀납 타입 T 아래의 중첩 출현을 제거할 때, 해당 파라미터가 생성자 필드에 언급되지 않는 팬텀(phantom) 파라미터인 경우 생성된 보조 타입에서 사라져 타입 검사를 우회할 수 있었다. 이를 통해 커널이 False의 증명을 수용하도록 유도 가능했다. 단, 이 버그는 메타프로그래밍을 통해 귀납 선언을 커널에 직접 전달해야만 도달할 수 있으며, 프론트엔드는 해당 비정상 항(term)을 정상적으로 차단한다.
**외부 검사기 nanoda와의 관계**: 해당 증명은 1주일 전 구버전의 nanoda(Rust로 구현된 독립 Lean 커널 검사기)도 통과했다. nanoda는 공식 커널의 누락 검사 부분은 확인했으나, 프로젝션 노드의 타입명 검증을 하지 않는 별개의 버그가 존재했다. nanoda 버그는 Jeremy Chen이 보고하고 Lean 버그 보고 1주 전 수정됐다. 두 개의 독립적인 버그가 동시에 존재했으나, 현재 버전의 두 구현체를 모두 사용하면 독립 검사의 유효성은 유지된다.
**lean4lean 영향**: Mario Carneiro의 lean4lean도 귀납 타입 처리가 참조 구현을 포팅한 것이어서 동일 버그에 영향을 받았으며, 해당 부분 검증 완료 시 발견됐을 것으로 분석됐다.
**메타프로그래밍 제한 논의**: 일부에서 메타프로그래밍 제한을 제안했으나, 개발팀은 이를 부적절한 접근으로 간주했다. 정교화기(elaborator)는 설계상 비신뢰 컴포넌트이며, 커널 자체가 비정상 선언을 독립적으로 거부해야 한다고 밝혔다.
수정 후 Kernel Arena에 회귀 테스트가 추가됐으며, 후속 PR #14582로 중첩 출현의 파라미터 동작 검증이 강화됐다.