- 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개를 찾아낸 대조군, 그리고 이 증명들이 보장하지 않는 것들(앨리어싱, 데이터 레이스, 제네릭, 종료성)을 정리합니다. 결론은 형식 검증이 만능이라는 것도, 쓸모없다는 것도 아닙니다 — 값이 어디서 나오는지가 코드베이스의 기존 테스트 성숙도에 달려 있다는 것입니다.