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