Skip to content

Formal-methods

  • Published on
    AWS와 Rust Foundation이 주도한 verify-rust-std 캠페인의 결과 논문이 2026년 NASA Formal Methods Symposium에 실렸습니다. 저자들이 "소프트웨어 라이브러리를 대상으로 보고된 것 중 가장 큰 검증 캠페인"이라 부르는 이 작업은 자동 생성 하네스 16,748개를 만들어 11,970개를 통과시켰지만, 표준 라이브러리에서 알려지지 않은 메모리 안전성 취약점은 하나도 찾지 못했습니다. 논문은 이 널 결과를 숨기지 않고 4.4절 제목으로 내걸고, 그 이유를 러스트의 기존 테스트와 Miri 동적 분석이 이미 잘 작동하고 있기 때문이라고 설명합니다. 이 글은 그 캠페인의 실제 숫자, 검증이 아니라 랜덤 테스트가 잡아낸 유일한 코드 버그, 같은 도구(Kani)가 s2n-quic·Firecracker·Cedar·Hifitime에서는 테스트와 퍼징이 놓친 버그 11개를 찾아낸 대조군, 그리고 이 증명들이 보장하지 않는 것들(앨리어싱, 데이터 레이스, 제네릭, 종료성)을 정리합니다. 결론은 형식 검증이 만능이라는 것도, 쓸모없다는 것도 아닙니다 — 값이 어디서 나오는지가 코드베이스의 기존 테스트 성숙도에 달려 있다는 것입니다.
  • Published on
    2026년, 정리 증명기(proof assistant)는 더 이상 학계의 비밀 무기가 아니다. Lean 4는 Leonardo de Moura가 AWS로 옮긴 뒤 폭발적으로 성장했고, mathlib는 100만 개 정리를 넘기며 Terence Tao를 비롯한 일급 수학자들의 일상 도구가 되었다. Coq는 2024년 3월 Rocq로 리브랜드를 마쳤고, Agda·Idris 2·Isabelle/HOL은 각자의 자리를 지킨다. Microsoft의 F*는 HACL* 암호 라이브러리를 검증해 Firefox와 Linux 커널에 실제로 들어갔고, Liquid Haskell은 refinement type으로 일반 코드를 검증한다. 그 위로 AI가 올라탔다 — DeepMind AlphaProof는 IMO 2024에서 은메달을, Anthropic은 AIMO ($5M 상금)와 mathlib search에 합류했다. Terence Tao는 Lean과 GitHub Copilot으로 자기 논문을 형식화하고 있다. Z3·CVC5 SMT 솔버가 그 밑단을 받치고, seL4·CompCert·IronFleet는 형식 검증이 실제 시스템에서 작동함을 증명한다. 한국의 KAIST·ETRI, 일본의 京都大学·東京大学·AIST가 그 흐름을 따라간다. 이 글은 2026년 정리 증명기 생태계 전체를 한 자리에 정리한다.