Lean, 이제 검증된 커널과 함께 배포된다

Lean Now Ships with Verified Kernels

Lean v4.35.0부터 `lake check` 명령으로 개발 내용을 샌드박스에서 공식 커널로 재검사할 수 있다. nanoda, lean4lean, con-leche, con-ron 등 네 가지 커널이 추가되어 `--paranoid` 옵션으로 모두 동시에 검사할 수 있다. 특히 Lean으로 작성되어 일관성이 증명된 첫 커널인 con-leche는 Claude가 Joachim Breitner의 감독 아래 구현했으며, Rust로 번역된 con-ron과 함께 사용하면 컴파일러나 런타임 버그로 인한 불건전성 위험을 크게 줄일 수 있다. 앞으로 lean4lean 검증도 완료될 예정이다.