Lean에 검증된 커널이 함께 배포됩니다
Lean v4.35.0은 개발 내용을 여러 커널로 다시 검사하는 `lake check`를 제공합니다. Lean으로 작성하고 일관성을 증명한 con-leche와 Rust로 옮겨 검증한 con-ron을 포함해 검사 경로를 늘렸으며, 정식 배포 커널과 구현·컴파일러의 오류가 증명 결과에 끼칠 위험을 줄이는 데 초점을 둡니다.
최신기사
AI, 개발 도구, 오픈소스, 보안과 인프라의 변화와 이용 조건을 설명하는 최신 기사와 해설입니다.
Creusot 0.14.0 출시 - Rust 계약을 형식 검증으로 증명하기
Rust 형식 검증 도구 Creusot 0.14.0이 부분 순서 명세, 스냅샷의 검증 조건 생성, rust-analyzer의 Pearlite 명세 이동 기능을 추가했습니다. 프로그램 코드와 증명 명세를 분리해 다루면서 증명 오류를 일찍 찾고 명세 안에서 정의를 탐색하기 쉬워졌습니다.
네 가지 정리 증명기의 이야기 — Isabelle/HOL, Lean, HOL4, Agda 비교
저자는 네 정리 증명기에서 유클리드 방식으로 소수의 무한성을 증명하고, 자동화·증명 과정 확인·정리 검색·사용 경험을 비교합니다. Isabelle/HOL과 HOL4는 자동화가 강하고, Agda는 증명 과정을 명시적으로 드러내지만 수작업이 많다는 평가입니다.
TLA+가 검증할 수 있는 것과 없는 것
TLA+는 동시성 시스템의 불변식과 생존 속성을 검증하는 데 유용하지만, 모든 시스템 속성을 표현하지는 못합니다. 글은 도달 가능성, 여러 실행 경로를 비교하는 하이퍼속성 등 표현의 한계를 짚고, 우회 기법에도 비용이 따른다고 설명합니다.
FrontierMath, 아페리식 무리수성 문제를 해결로 표시
FrontierMath가 ζ(5)의 무리수성을 증명하는 해답을 확인해 문제를 해결로 표시했습니다. 해답은 문제에서 찾도록 한 아페리(Apéry)식 점화식을 사용하지 않으며, FrontierMath는 AI 시스템의 정체를 모르는 상태에서 인간과 AI가 함께 만든 결과로 판정했습니다.
Skia를 위한 컴파일러 스타일 드로잉 최적화 — 2D 래스터화 의미론으로 검증합니다
Skia 같은 래스터화 라이브러리는 빠르지만 애플리케이션이 전달하는 연산 순서가 비효율적일 수 있습니다. 연구진은 Skia의 동작을 Lean으로 형식화한 μSkia를 만들고, Chrome에서 발견한 네 가지 최적화를 검증해 99개 웹사이트 프로그램에서 최대 32μs의 분석 비용으로 18.7% 속도 향상을 얻었습니다.