태그: #formal-methods

한국어English日本語中文

← 전체 글

• 러스트 표준 라이브러리 검증 캠페인이 찾아낸 메모리 안전성 버그는 0개였다

  AWS와 Rust Foundation이 주도한 verify-rust-std 캠페인의 결과 논문이 2026년 NASA Formal Methods Symposium에 실렸습니다. 저자들이 "소프트웨어 라이브러리를 대상으로 보고된 것 중 가장 큰 검증 캠페인"이라 부르는 이 작업은 자동 생성 하네스 16,748개를 만들어 11,970개를 통과시켰지만, 표준 라이브러리에서 알려지지 않은 메모리 안전

  2026-07-16 · 48 분 읽기 #formal-methods#rust#verification#memory-safety#testing

• Lean 4 & 정리 증명기 2026 — mathlib / Rocq (구 Coq) / Agda / Isabelle / FStar / AlphaProof / AIMO 심층 가이드

  2026년, 정리 증명기(proof assistant)는 더 이상 학계의 비밀 무기가 아니다. Lean 4는 Leonardo de Moura가 AWS로 옮긴 뒤 폭발적으로 성장했고, mathlib는 100만 개 정리를 넘기며 Terence Tao를 비롯한 일급 수학자들의 일상 도구가 되었다. Coq는 2024년 3월 Rocq로 리브랜드를 마쳤고, Agda·Idris 2·Isabelle/HOL

  2026-05-16 · 37 분 읽기 #lean-4#lean#mathlib#rocq#coq