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

• 들어가며 — 사상 최대 규모라는 검증 캠페인의 결과
• 무엇을 검증하려 했나
• 캠페인의 구조 — 현상금이 걸린 오픈 콘테스트
• 숫자 — 33,955개 함수 중 어디까지 갔나
• 실제로 찾은 것 — 표 2에 적힌 네 줄
• 널 결과를 어떻게 읽을 것인가
• 대조군 — 같은 도구가 다른 코드베이스에서는
  • try_fit — 1,677만 번의 퍼징이 못 넘은 벽을 20초에
  • 테스트가 원리상 볼 수 없는 것 — Firecracker
  • Cedar — 형식 참조 모델도 못 막은 것
• 계약이 연 문 — 그리고 버그를 긍정하고 있던 테스트
• LLM이 명세를 쓸 때 — 측정된 결과
• 정직한 한계 — 이 증명들이 보장하지 않는 것
• 비용
• 그래서 언제 쓰고, 언제 쓰지 않아야 하나
• 마치며
• 참고 자료

들어가며 — 사상 최대 규모라는 검증 캠페인의 결과

형식 검증 이야기는 보통 이렇게 끝납니다. "그래서 아무도 못 찾던 치명적 버그를 찾았습니다." 그래서 이 논문의 4.4절 제목과 첫 문장은 좀 낯섭니다.

The verification effort has not uncovered any previously unknown memory safety vulnerabilities in the standard library.

2026년 6월 16일 arXiv에 올라오고 NASA Formal Methods Symposium 2026에 게재된 Verifying the Rust Standard Library의 문장입니다. 저자 목록에는 AWS의 Byron Cook을 비롯해 Rust Foundation, UCL, KU Leuven, UCSD, 런던 퀸메리, MIT 소속이 섞여 있습니다. 저자들 표현으로 "소프트웨어 라이브러리를 대상으로 보고된 것 중 가장 큰 검증 캠페인"(저자 자체 평가입니다)의 결론이 "새로 찾은 메모리 안전성 취약점 없음"인 것입니다.

이건 실패담이 아닙니다. 그리고 성공담도 아닙니다. 형식 검증이 실무에서 실제로 어떤 값을 하는지에 대해, 홍보 자료보다 훨씬 유용한 데이터입니다. 이 글은 그 숫자를 그대로 읽어 보려고 합니다.

무엇을 검증하려 했나

러스트의 소유권 타입 시스템은 데이터 레이스와 상당수의 메모리 오류를 컴파일 타임에 막습니다. 문제는 표준 라이브러리 자신이 unsafe 코드에 크게 의존한다는 점입니다. 컴파일러가 검사하지 않는 다섯 가지 연산 — 원시 포인터 역참조, unsafe 함수 호출, 가변 static 접근, unsafe 트레이트 구현, union 필드 접근 — 의 건전성은 결국 개발자의 추론에 달려 있고, 그 추론은 대개 자연어 SAFETY 주석으로만 기록됩니다.

논문이 인용하는 규모 감각은 이렇습니다. 지난 3년간 I-unsound 라벨로 보고된 건전성 버그가 74건이 넘고, 역사적으로 CVE는 18건이 등록됐습니다(둘 다 2026년 3월 기준). 러스트가 커널·브라우저 엔진·암호 라이브러리에 들어가는 지금, 이 기반을 기계로 검증된 증명으로 받치자는 게 캠페인의 동기입니다.

여기서 용어를 정확히 해 둘 필요가 있습니다. 이 캠페인이 목표로 하는 건 미정의 동작(UB)의 부재이지 완전한 정확성이 아닙니다. UB 부재는 메모리 안전성의 충분조건이지만, 기능적 정확성·라이브니스·보안 속성까지 보장하지는 않습니다.

캠페인의 구조 — 현상금이 걸린 오픈 콘테스트

표준 라이브러리는 한 팀이 검증하기엔 너무 큽니다. 그래서 Rust Foundation이 운영하는 오픈 콘테스트로 설계했습니다.

검증 과제는 챌린지(challenge) 단위로 쪼개집니다. 각 챌린지는 구체적 검증 대상, 가정 목록, 명시적 성공 기준, 그리고 완료 시 지급되는 현상금을 정의합니다. 참가자가 포크해서 PR을 내면 기술 검토 위원회가 리뷰하고, 승인되면 model-checking/verify-rust-std 포크에 병합됩니다. 논문 기준(2026년 3월)으로 챌린지 29개가 공개됐고, 최소 4개 기관 소속 외부 기여자 21명 이상으로부터 PR 450건 이상을 받았습니다.

이 숫자는 저장소에서 직접 확인됩니다. doc/src/challenges/ 아래에 0001-core-transmutation.md부터 0029-boxed.md까지 정확히 29개가 있고, 저장소는 지금도 살아 있습니다.

콘테스트는 도구 중립적입니다. 러스트 표준 라이브러리에서 돌고, CI에 통합되고, (보통 동료 심사 논문으로 뒷받침되는) 명확한 건전성 보장을 제공하면 어떤 도구든 받습니다. 현재 지원 도구는 넷입니다.

• Kani — CBMC 기반 유계 모델 체킹. 캠페인의 주력.
• ESBMC — 역시 모델 체킹.
• Flux — 정제 타입(refinement type)으로 수치 범위와 안전성 선행조건을 검사.
• VeriFast — 분리 논리(separation logic). 다루는 함수에 한해 포인터 앨리어싱 위반을 포함한 모든 UB의 부재를 검증.

Verus, Creusot, KRust, RAPx 넷은 검토 중입니다. 논문이 강조하는 건, 이 다양성이 취향 문제가 아니라 필연이라는 점입니다 — 아키텍처별 인트린식, 포인터 중심 코드, 동시성 프리미티브, 복잡한 불변식을 가진 루프는 서로 다른 추론 기법을 요구합니다. 단일 도구로는 모든 검증 조건을 소화할 수 없습니다.

숫자 — 33,955개 함수 중 어디까지 갔나

nightly-2025-10-08 툴체인 스냅샷 기준으로 core, alloc, std 세 크레이트에는 함수가 33,955개 있습니다.

처음 16개월은 손으로 증명을 썼습니다. Kani 하네스 725개(그중 694개가 함수 계약 포함), VeriFast 증명 50개 이상. 그리고 2025년 10월경 새 계약의 증가율이 평평해집니다. 논문의 진단은 냉정합니다 — 수작업 증명 엔지니어링만으로는 수만 개 함수에 도달할 수 없다는 근본적 확장성 한계입니다.

그래서 만든 게 Autoharness입니다. Kani 안의 컴파일러 패스로, 크레이트의 모든 함수를 열거해 자격을 판정하고, 통과한 함수마다 완전히 비결정적인 입력으로 호출하는 증명 하네스를 MIR 수준에서 합성합니다. 소스는 건드리지 않습니다 — 그래서 CI에 넣을 수 있습니다.

하네스는 유닛 테스트와 비슷하지만, 구체적 입력 대신 모든 가능한 입력을 동시에 대표하는 심볼릭 값으로 함수를 호출합니다. 모델 체커가 도달 가능한 모든 실행 경로를 남김없이 탐색하면, 테스트가 아니라 형식 검증 문제가 됩니다.

전체 함수                    33,955
├─ Autoharness 하네스 생성   16,748
│   ├─ 검증 통과             11,970
│   └─ 실패                   4,778   (모델 부재 / 타임아웃 / 미지원)
└─ 건너뜀                    17,207
    ├─ 제네릭 타입 파라미터    9,635  (56%)
    ├─ Arbitrary 구현 없음     3,826  (22%)
    ├─ Kani 내부 함수          3,246  (19%)
    └─ 기타                      500  (3%)

통과한 11,970개를 범주별로 쪼개면 이렇습니다.

여기서 논문이 스스로 붙인 단서가 중요합니다. 통과한 11,970개가 모두 같은 무게의 증거는 아닙니다.

수작업 계약 증명 694개를 더하면 형식 함수 계약으로 검증된 함수는 989개(자동 295 + 수동 694)이고, 이게 캠페인이 제공하는 가장 강한 보장입니다. 33,955개 중 989개, 약 2.9%입니다.

반대쪽 끝에는 계약 없이 통과한 unsafe 함수 622개가 있습니다. 논문의 해석은 이렇습니다 — 이 함수들이 통과했다는 건 (a) Kani가 검사하는 UB 부류에 대해 자명하게 안전하고 그 함수의 unsafe 표시는 Kani가 아직 검사하지 않는 앨리어싱 같은 속성 때문이거나, (b) 그 함수의 실제 동작에 대해 Kani의 UB 커버리지가 불완전하거나 둘 중 하나입니다. 둘을 구분하려면 사람이 봐야 합니다. 논문은 이 622개를 증명이 아니라 "자동 분류가 떠올린 후보"로 부릅니다.

중간이 가장 튼튼합니다. 통과한 안전 함수 10,194개(Autoharness 통과분의 85%)는 모호함이 없습니다. Kani가 전이적으로 도달하는 unsafe 코드까지 포함해 모든 피호출자를 심볼릭 실행하면서, 비트 유효한 모든 입력에 대해 어떤 경로도 UB를 일으키지 않음을 확인한 것이니까요.

실제로 찾은 것 — 표 2에 적힌 네 줄

그래서 이 모든 작업이 찾아낸 이슈 전체가 표 2입니다.

네 줄입니다. 그리고 이 중 셋은 코드 버그가 아니라 명세와 문서의 문제입니다 — 누락된 안전성 표기, 틀린 SAFETY 주석, 함수 동작을 잘못 서술한 문서.

논문은 이걸 부차적 이득으로 정직하게 자리매김합니다. 형식 명세를 쓰는 행위 자체가 자연어 주석만으로는 나오지 않는 안전성 요구사항의 정밀한 표현을 강제한다는 것입니다. 실제로 이 효과는 러스트 언어 자체에 흔적을 남겼습니다 — 언어 팀이 계약(contract)을 실험적 언어 기능으로 받아들였고, Rust 프로젝트는 표준 라이브러리에 안전성 계약을 다는 공식 목표를 채택했습니다.

그런데 유일하게 코드 버그인 첫 줄, "잘못된 SIMD 시프트 결과"에 반전이 있습니다. 논문 7절이 직접 밝힙니다 — 챌린지 15는 SIMD 인트린식 565개의 실행 가능 모델에 대한 랜덤 테스트로 완료됐지 형식 증명으로 완료된 게 아닙니다. 재현을 위해 시드를 로깅했고 업스트림 버그 두 건을 찾아냈지만, 저자들 표현으로 이건 "형식 검증이 아니라 높은 신뢰도의 검증(validation)"으로 읽어야 합니다.

정리하면 이렇습니다. 사상 최대 규모의 검증 캠페인이 표준 라이브러리에서 찾은 코드 버그는, 형식 검증이 아니라 랜덤 테스트가 찾았습니다.

널 결과를 어떻게 읽을 것인가

논문 자신의 해석부터 옮깁니다.

This null result is itself informative: it speaks to the effectiveness of Rust's existing testing infrastructure and Miri-based dynamic analysis at catching memory safety bugs before they reach production.

즉 "형식 검증이 쓸모없다"가 아니라 "러스트 표준 라이브러리의 기존 테스트가 이미 대단히 좋다"는 신호로 읽습니다. Miri는 이미 표준 라이브러리에서 수십 개의 버그를 찾아냈고 CI에 통합돼 있습니다. 새로 찾을 게 별로 안 남아 있었던 겁니다.

그리고 캠페인의 값을 다시 정의합니다.

Testing can demonstrate the absence of bugs on exercised inputs; verification certifies their absence on all inputs within scope.

테스트는 실행해 본 입력에 대해 버그의 부재를 보일 수 있고, 검증은 범위 안의 모든 입력에 대해 부재를 증명합니다. 그러니까 캠페인의 산출물은 버그 목록이 아니라 CI에 상주하는 기계 검사 증명입니다. 매 PR마다 전체 도구 스위트가 활성 증명 전부에 대해 돌고, 위반이 생기면 즉시 잡힙니다. 회귀 방지 장치입니다.

이 주장은 정직하긴 한데, 냉정하게 보면 이런 뜻이기도 합니다 — 이 캠페인의 ROI는 미래에 있습니다. 이미 없는 버그를 찾아 준 게 아니라, 앞으로 들어올 버그를 막겠다는 것이고, 그 값은 아직 측정되지 않았습니다.

대조군 — 같은 도구가 다른 코드베이스에서는

여기서 끝났다면 "형식 검증은 잘 테스트된 코드에는 별 소용없다"로 마무리했을 겁니다. 그런데 2주 뒤인 2026년 7월 1일, 같은 팀 상당수가 Kani: A Model Checker for Rust를 올렸습니다(아직 프리프린트입니다). 이 논문의 표 2가 정확히 대조군입니다.

Kani는 프로덕션 러스트 코드베이스 네 곳에서 테스트와 퍼징이 놓친 버그 11개를 찾았습니다.

같은 도구, 정반대 결과입니다. 차이는 도구가 아니라 대상 코드의 기존 테스트 성숙도입니다.

try_fit — 1,677만 번의 퍼징이 못 넘은 벽을 20초에

가장 인상적인 사례입니다. s2n-quic은 아마존의 IETF QUIC 구현이고, try_fit 함수는 패킷의 남은 용량이 주어졌을 때 QUIC Stream 프레임에 데이터를 몇 바이트 넣을지 결정합니다. 프레임 길이의 가변 길이 정수 인코딩이 용량 경계에서 커지기 때문에 미묘한 계산입니다.

s2n-quic은 Bolero 프로퍼티 테스트 프레임워크를 씁니다. #[cfg_attr(kani, kani::proof)] 어트리뷰트 하나로 같은 하네스가 퍼즈 테스트로도, Kani 증명으로도 돕니다. 그래서 다음 비교가 성립합니다 — 구현을 참조 모델과 비교하는 차등 Bolero 하네스를 libfuzzer로 10분 넘게, 16,777,216회 실행했지만 실패를 못 찾았습니다. Kani는 20초 만에 실패하는 어서션을 찾았습니다.

실패 지점은 1바이트 인코딩과 2바이트 인코딩의 경계 근처였습니다. 논문의 진단이 핵심입니다 — 커버리지 유도 퍼징이 그쪽으로 향할 기울기(gradient)가 없는 희소한 입력 공간이고, Kani의 심볼릭 실행은 거기로 직행합니다.

두 번째 s2n-quic 사례는 반대로 상보성을 보여 줍니다. decode_packet_number 버그는 Kani가 2.8초에, 퍼징이 1분 안에 독립적으로 찾았습니다. 둘 다 찾은 경우에도 Kani 쪽이 더 실행 가능한 정보를 줍니다 — 정체불명의 크래시가 아니라 이름 붙은 속성의 실패를 지목하고, concrete playback 기능으로 개발자가 평범한 러스트 테스트로 재생할 수 있는 구체적 반례를 생성합니다.

테스트가 원리상 볼 수 없는 것 — Firecracker

Firecracker는 AWS Lambda와 Fargate 뒤에 있는 VMM입니다. Kani를 보안 핵심 컴포넌트 둘에 씁니다.

I/O 레이트 리미터는 토큰 버킷입니다. 관심 있는 속성은 "마이크로VM이 어떤 1초 구간에서도 설정된 I/O 대역폭을 초과할 수 없다"입니다. 그런데 이건 본질적으로 시간 의존적입니다 — 보충되는 토큰 수가 auto_replenish가 시스템 클럭 대비 언제 호출되느냐에 달려 있어서, 남김없이 테스트하는 게 불가능합니다.

Kani의 해법은 libc::clock_gettime을 단조 비감소 Instant를 반환하는 비결정적 스텁으로 갈아 끼우는 것입니다. 시간 차원 자체를 심볼릭 변수로 바꿔 버립니다. 이렇게 만든 하네스가 레이트 리미터에서 여러 버그를 찾았고, 가장 중요한 건 적대적으로 타이밍을 맞춘 호출에서 게스트가 자기 I/O 예산을 최대 0.01%까지 초과할 수 있게 하는 반올림 오류였습니다.

여기서 정직하게 짚을 게 있습니다. 0.01%는 실무적으로 아주 작은 초과입니다. 이걸 "치명적 취약점"으로 포장하면 거짓말입니다. 흥미로운 건 크기가 아니라 종류입니다 — 이 오류는 보충 호출이 시스템 클럭 대비 밀리초 이하 수준에서 정확히 언제 일어나는지에 달려 있고, 이건 테스트가 결정론적으로 제어할 수 없고 퍼징도 명시적 시간 모델 없이는 겨냥할 수 없는 조건입니다.

두 번째는 VirtIO 장치 에뮬레이션입니다. 호스트와 게스트가 공유하는 메모리는 적대적 공격면입니다 — 신뢰할 수 없는 게스트가 공유 디스크립터와 링 버퍼에 임의 값을 쓸 수 있습니다. Kani는 비결정적 게스트 메모리로 이 시나리오를 표현해 VirtIO 명세 2.6.7.2절 준수를 검증했고, 게스트가 VirtIO 큐 컴포넌트의 시작 주소를 MMIO 갭에 놓아 Firecracker를 부팅 중 panic시킬 수 있다는 버그를 추가로 찾았습니다.

Cedar — 형식 참조 모델도 못 막은 것

Cedar는 오픈소스 인가 정책 언어이자 엔진입니다. 이 사례가 특별한 건 Cedar가 이미 형식 참조 모델에 대한 차등 테스트를 하고 있었다는 점입니다. 그런데도 버그가 프로덕션 코드까지 살아남았습니다.

contains_at_least_two는 문자열에 특정 부분 문자열이 두 번 이상 나오는지 검사합니다. 멀티바이트 문자를 검색어로 넘기면 &str을 문자 경계가 아닌 곳에서 자를 수 있고, 런타임 panic이 납니다. 기존 테스트 전부에서 조용했습니다. Kani의 심볼릭 실행이 반례를 만들었고, 수정은 cedar PR 1037로 병합됐습니다(2024년 7월).

날짜에 주의하세요. Kani 논문은 2026년이지만 개별 사례의 연식은 제각각입니다 — Cedar 수정은 2024년 건입니다. 논문이 2026년에 이 사례들을 묶어 보고한 것이지, 11개가 전부 2026년에 발견된 게 아닙니다.

계약이 연 문 — 그리고 버그를 긍정하고 있던 테스트

Hifitime은 고정밀 시간 관리 라이브러리이고, Firefly의 Blue Ghost Mission 1 달 착륙 임무에 쓰였습니다. 여기가 Kani 논문의 계약(contract) 사례 연구입니다.

Kani의 계약은 함수 선행조건·후행조건·루프 불변식을 러스트 불리언 식으로 씁니다. 이게 왜 중요하냐면, 유계 모델 체킹을 무계 보장으로 끌어올리기 때문입니다 — 루프를 남김없이 펼치는 대신 불변식이 귀납적임을 검증하고 그걸로 루프를 추상화합니다. 논문 표현으로 1단계는 연산이 크래시하지 않음을 증명하고, 2단계는 연산이 올바르게 계산함을 증명합니다.

기능적 속성을 세우는 부수 효과로 Kani는 이전에 알려지지 않은 버그 6개를 찾았습니다. panic 부재 하네스로는 표현조차 할 수 없던 속성들입니다. 가장 의미 있는 둘은 러스트 표준 라이브러리 자신의 요구를 위반한 것들이었습니다.

• Epoch의 PartialEq/Ord 불일치. Duration::PartialEq는 부호가 반대인 값을 의도적으로 같다고 봅니다(방향과 무관한 구간 길이를 나타내니까). 그런데 Epoch::PartialEq가 이 구현에 위임한 반면 Epoch::Ord는 부호를 구분하는 사전식 비교를 썼습니다. 러스트 표준 라이브러리는 a == b이면 a.cmp(b)가 Ordering::Equal이어야 한다고 요구합니다. 부호가 다른 모든 에포크 쌍에서 이 불변식이 깨져 있었습니다.
• Duration의 PartialEq/Ord 불일치(영점 교차). 같은 뿌리입니다. 두 Duration이 a == b와 a < b를 동시에 만족할 수 있었습니다.

Epoch 버그가 왜 테스트에 안 잡혔는지가 이 글의 요점을 압축합니다 — 어떤 테스트도 에포크를 그 부호 반전과 비교하지 않았기 때문입니다. "시점"에 대해 개념적으로 이상한 연산이라서요. Kani의 심볼릭 실행은 모든 가능한 Epoch 쌍을 탐색하면서 이 입력을 자동으로 만들어 냈습니다.

그리고 가장 뼈아픈 디테일. total_nanoseconds() 부호 오류(음의 방향으로 한 세기를 넘는 기간에서 덧셈 대신 뺄셈을 씀)를 계약이 잡았을 때, 수정은 소스 한 글자였습니다. 그런데 기존 통합 테스트 하나가 그 버그 동작을 옳다고 어서션하고 있었고, 구현과 함께 고쳐야 했습니다. 논문의 진단이 날카롭습니다 — 테스트 오라클이 구현의 출력을 보고 작성됐기 때문에 같은 오류를 그대로 인코딩하고 있었던 것입니다. 후행조건은 Duration 타입의 인코딩 불변식에서 유도됐기 때문에 구현과 테스트 양쪽을 독립적으로 검사할 수 있었습니다.

이 함정은 논문 밖에서도 확인됩니다. Hifitime 저장소의 이슈 475는 Kani 검증 작업(PR 474, 2026년 4월 병합) 중에 발견된 try_truncated_nanoseconds의 오류 분류 버그인데, 이슈 본문이 이렇게 적고 있습니다 — "증명이 통과하도록 Kani 하네스를 현재의 (잘못된) 동작에 맞춰 갱신했고, 실제 구현은 따로 고쳐야 한다." 명세를 구현에 맞추면 검증은 통과하고 버그는 남습니다. 검증 도구가 있어도 사람이 명세를 어디서 가져오는지가 여전히 전부입니다.

LLM이 명세를 쓸 때 — 측정된 결과

Hifitime 2단계 명세는 셸 접근 권한을 가진 AI 코딩 어시스턴트로 개발됐습니다. 워크플로는 타이트한 루프였습니다 — 어시스턴트가 계약 어노테이션을 제안하고, 소스에 쓰고, cargo kani를 돌리고, 결과(성공/실패/타임아웃/컴파일 오류)를 보고, 명세를 다듬습니다. 사람 연구자는 어떤 함수를 겨냥할지 지시하고, 도메인 맥락을 주고, 제안된 계약의 타당성을 리뷰했습니다.

Kani의 명세 언어가 러스트의 확장이라는 점이 여기서 유리하게 작용합니다. 계약이 러스트 불리언 식이고 하네스가 러스트 함수라서, 어시스턴트가 별도의 형식 언어를 배우지 않고 기존 러스트 지식을 그대로 씁니다.

논문이 강조하는 건 결과보다 구조입니다.

Crucially, the specifications do not need to be trusted: Kani verifies every contract against the implementation.

명세를 신뢰할 필요가 없다는 것입니다. 실제로 AI가 생성한 계약 3개가 검증에 실패했고, Kani가 셋 다 잡았습니다.

1. 검증 대상 함수를 자기 ensures 절에서 호출하는 감당 불가능한 후행조건 — SAT 식이 두 배가 되면서 솔버 타임아웃. (어시스턴트가 직접적인 산술식으로 단순화)
2. 지나치게 넓은 심볼릭 입력(kani::any::<Epoch>())이 TimeScale::ET 변형을 포함해 sin()을 SAT 식으로 끌어들이면서 타임아웃. (TimeScale::TAI로 제한)
3. const fn 비호환 — Kani의 매크로 확장이 non-const 코드를 생성해 컴파일 오류. (독립 증명 하네스로 전환)

분류하면 명세 설계 오류 하나, 하네스 설계 오류 하나, Kani 자체 한계 하나입니다. 셋 다 어시스턴트가 Kani 출력만 보고 같은 세션 안에서 진단하고 고쳤습니다.

이게 LLM 증명 자동화 이야기 중 드물게 정직한 축입니다 — 자랑거리가 "AI가 명세를 잘 쓴다"가 아니라 "AI가 명세를 틀리게 써도 검증기가 걸러낸다"입니다. 사람이 검토했다면 놓쳤을 수 있는 것을 Kani가 잡았다는 점(논문 표현으로 "all caught by Kani, not human review")이 핵심입니다.

한편 표준 라이브러리 캠페인 쪽의 LLM 실험은 훨씬 조심스럽습니다. 자연어 SAFETY 주석을 함수 계약으로 번역하는 LLM 기반 계약 합성을 시도했지만, 논문은 이걸 "예비적(preliminary)"이라 부르고, 생성된 계약은 병합 전 수동 검토가 필요하며, 정밀도와 재현율의 체계적 평가는 향후 과제로 남겼습니다. 여기에 대해 인용할 만한 숫자는 아직 발표되지 않았습니다.

정직한 한계 — 이 증명들이 보장하지 않는 것

NFM 논문 7절은 제목이 "Limitations and threats to validity"이고, 형식 검증 홍보 글에서 보기 힘든 밀도로 쓰여 있습니다. 그대로 옮길 가치가 있습니다.

유계 추론. Kani는 기본적으로 유계 모델 체킹입니다 — 루프를 설정된 한도까지 펼칩니다. 한도가 부족하면 언와인딩 어서션이 실패해 증명이 실패로 보고되니 조용히 틀리진 않습니다. 하지만 종료성은 검증하지 않습니다. Kani가 아직 루프 변량(decreases) 절을 지원하지 않기 때문입니다.

부분적인 속성 커버리지. Kani는 러스트 레퍼런스가 나열하는 UB의 부분집합만 검사합니다. 검사하지 않는 것들이 만만치 않습니다.

• 포인터 앨리어싱 모델(Stacked Borrows / Tree Borrows) 위반
• 데이터 레이스
• 잘못된 인라인 어셈블리
• 프로버넌스 관련 UB의 일부 형태
• unsafe 경계를 넘나드는 타입 안전성 불변식의 보존 (예: Vec의 길이가 용량을 넘지 않는다는 것)

논문 문장 그대로 — 현재의 모든 검사를 통과한 함수도 더 완전한 모델 아래에서는 여전히 UB를 보일 수 있습니다.

명세와 모델의 공백. 러스트에는 아직 비준된 형식 명세가 없습니다. 앨리어싱 모델 같은 핵심 부분은 경쟁하는 제안들이 있고, 향후 명세가 바뀌면 오늘의 가정 아래 건전했던 증명이 무효가 될 수 있습니다. 인트린식과 외부 함수를 호출하는 함수의 검증은 그 연산에 제공된 모델의 충실도에 의존하고, 모델이 부정확하면 건전하지 않은 검증 결과가 나올 수 있습니다.

툴체인 건전성. 모든 결과가 도구의 정확성에 의존합니다 — Kani의 MIR-to-GOTO 변환, CBMC, 호출되는 SAT/SMT 솔버, VeriFast의 심볼릭 실행 엔진. 논문이 직접 씁니다. 이 도구들 중 어느 것도 그 자신이 형식 검증되지 않았습니다. 신뢰성은 광범위한 테스트와 퍼징, 수년간의 프로덕션 사용에 기대고 있습니다.

동시성은 아예 공백입니다. 29개 챌린지 중 둘이 동시성 API를 겨냥합니다 — 챌린지 7(atomic 타입)과 챌린지 27(Arc). 둘 다 승인된 해답이 하나도 없습니다. unsafe 러스트의 데이터 레이스는 즉시 UB인데도 그렇습니다. 어려운 건 완화된 메모리 모델 아래에서 락프리 자료구조를 명세하고 검증하는 일입니다.

남은 영역. 1만 개 넘는 함수를 검증했지만 표준 라이브러리는 완전 검증과 거리가 멉니다. BTreeMap 내부, atomic 타입, String, 이터레이터, 벡터, 데크, 참조 카운트 타입 등 영향력 큰 API 상당수가 부분적으로만 다뤄졌거나 아직 손도 못 댔습니다.

Kani 논문도 자기 사례 연구의 편향을 인정합니다 — 평가 대상 프로젝트들은 무작위 표본이 아니라 스스로 Kani를 채택한 곳들이라 유리한 사례가 과대 대표됐을 수 있습니다. Cedar 실험이 Kani를 쓰지 않던 프로젝트에 대한 의도적 평가라서 이걸 부분적으로 완화한다고 씁니다.

비용

증명 유지보수. 검증 저장소는 업스트림 rust-lang/rust의 포크이고 주기적으로 동기화해야 합니다. 그런데 러스트는 6주마다 새 릴리스를 냅니다. 논문의 결론은 이 방식이 지속 가능하려면 계약과 증명을 업스트림에 올려서 증명 유지보수가 표준 개발 워크플로의 일부가 되어야 한다는 것입니다. 지금은 그렇지 않습니다.

컴파일 시간. 하네스가 폭증하면서 컴파일이 병목이 됐습니다. 전용 컴파일러 벤치마킹 도구를 만들고 병렬화·캐싱·휴리스틱 코드 생성 순서·함수 스터빙을 넣어 표준 라이브러리 컴파일에서 3.97배 속도 향상을 얻었습니다(저자 자체 측정, 나이브한 순차 파이프라인 대비).

CI 시간. Kani 논문 표 1 기준입니다.

대부분 25분 안에 끝납니다. PR 워크플로에 넣을 만한 예산이라는 게 논문 주장이고, 이 표를 보면 납득이 갑니다. 다만 하네스 수와 시간이 선형이 아니라는 점도 보입니다 — 하네스 1개짜리 rust-sel4가 4분, 10개짜리 zerocopy가 3분입니다. 하네스 개수보다 개별 증명의 난이도가 지배적입니다.

사람과 조직 비용. 논문 5.1절이 가장 솔직합니다. 초기 계획은 기술 마일스톤에 집중했는데, 커뮤니티 합의와 기관 조율에 드는 시간을 크게 과소 편성했다고 인정합니다. 계약을 러스트 컴파일러에 통합하려면 언어 팀·라이브러리 메인테이너·도구 저자의 광범위한 지지가 필요했고, 기술적으로 간단한 변경조차 이해관계자를 일찍 참여시키지 않으면 멈춰 섰습니다. 외부 기관과의 협업에는 몇 달이 걸리는 법적 합의가 필요했습니다. 외부 기여자를 끌어들이는 데도 현상금만으로는 부족했고 난이도 스펙트럼, 명확한 문서, 동작하는 예제가 필요했습니다.

도구별 오버헤드. VeriFast로 LinkedList를 증명한 PR 238(챌린지 5, 2025년 8월 병합)이 이 비용을 잘 보여 줍니다. 함수 19개를 직접 검증하고 5개의 건전성을 함의하는데, VeriFast는 고스트 명령을 넣기 위해 소스를 살짝 고쳐야 합니다(예: for 루프를 loop로, Option::map을 1차 등가물로). 그래서 CI 파이프라인이 3단계입니다 — VeriFast가 주석 달린 코드를 검사하고, 정제 검사기가 원본의 모든 동작이 주석 버전의 동작이기도 함을 기계적으로 검증하고, diff가 원본이 업스트림과 일치하는지 확인합니다. 모델 체킹 대비 연역적 검증이 지우는 엔지니어링 부담을 그대로 보여 주는 동시에, 더 깊은 보장(모든 UB의 부재)을 주는 대가이기도 합니다.

그래서 언제 쓰고, 언제 쓰지 않아야 하나

두 논문을 겹쳐 놓으면 판단 기준이 꽤 선명하게 나옵니다.

값을 하는 경우

• 기존 테스트가 원리상 닿을 수 없는 속성이 있다. 시간 의존 코드(Firecracker 레이트 리미터), 적대적 입력이 들어오는 공유 메모리 경계(VirtIO), 인코딩 경계 같은 희소한 입력 영역(try_fit). 퍼징에 기울기가 없는 곳이 정확히 심볼릭 실행의 자리입니다.
• 코드가 좁고 상태 공간이 명확하다. 표 1에서 CI가 짧은 프로젝트들의 공통점입니다.
• 속성을 명세로 적을 수 있다. Eq/Ord 일관성, 인코딩-디코딩 항등성처럼 구현과 독립적으로 유도 가능한 불변식이 있으면 계약이 진짜 값을 합니다. Hifitime 사례가 이걸 보여 줍니다.
• 회귀를 막는 게 목적이다. 이미 잘 테스트된 코드라도, CI에 상주하는 기계 검사 증명은 앞으로의 회귀를 잡습니다. 표준 라이브러리 캠페인이 실제로 사는 지점입니다.
• 이미 프로퍼티 테스트가 있다. s2n-quic처럼 Bolero를 쓰고 있으면 어트리뷰트 하나로 같은 하네스가 증명이 됩니다. 한계 추가 비용이 거의 0입니다.

과잉이거나 아직 안 되는 경우

• 코드가 이미 Miri급으로 검증돼 있다. 표준 라이브러리 결과가 정확히 이 경우입니다. 새 버그를 기대하고 들어가면 실망합니다.
• 제네릭이 코드의 중심이다. Autoharness가 건너뛴 함수의 56%가 제네릭입니다. 러스트가 컴파일 타임에 단형화하기 때문에 미인스턴스화 타입 파라미터의 입력을 합성하지 못합니다.
• 동시성이 핵심이다. 챌린지 7과 27에 승인된 해답이 없다는 사실이 현재 성숙도를 말해 줍니다. 완화된 메모리 아래의 락프리 자료구조는 아직 열린 문제입니다.
• 앨리어싱·데이터 레이스가 주된 위험이다. Kani는 이걸 안 봅니다. 이 영역은 여전히 Miri가 담당합니다.
• 명세를 구현에서 베껴 올 참이다. 이슈 475와 Hifitime 버그 (i)이 보여 주듯, 구현을 보고 쓴 명세는 구현의 버그를 그대로 인코딩합니다. 이러면 검증은 통과하고 버그는 남습니다. 독립적으로 유도 가능한 명세가 없다면 검증은 값비싼 동어반복입니다.

한 문장으로 줄이면 이렇습니다. 형식 검증의 값은 도구의 강력함이 아니라, 당신의 기존 테스트가 못 닿는 영역이 얼마나 넓은지에 비례합니다.

마치며

이 두 논문이 같이 읽혀야 하는 이유가 여기 있습니다. 하나만 읽으면 틀린 결론이 나옵니다.

NFM 논문만 읽으면 "사상 최대 검증 캠페인이 버그를 0개 찾았다 — 형식 검증은 과대평가됐다"가 됩니다. Kani 논문만 읽으면 "1,677만 번의 퍼징이 놓친 걸 20초에 찾았다 — 왜 아직 안 쓰나"가 됩니다. 둘 다 같은 도구, 같은 팀의 결과입니다.

진짜 결론은 그 사이에 있습니다. 표준 라이브러리에서 버그가 안 나온 건 도구가 약해서가 아니라 대상이 이미 수년간 Miri와 테스트로 다져졌기 때문이고, s2n-quic과 Hifitime에서 버그가 나온 건 도구가 마법이어서가 아니라 그 코드에 테스트가 원리상 닿지 못하는 구석이 있었기 때문입니다. 형식 검증은 테스트의 상위 호환이 아니라 테스트와 상보적인 다른 모양의 그물입니다.

그리고 마지막으로, 이 캠페인이 남긴 가장 큰 자산은 증명 11,970개가 아닐지도 모릅니다. 계약이 러스트의 실험적 언어 기능이 됐고, 표준 라이브러리에 안전성 계약을 다는 게 프로젝트 공식 목표가 됐습니다. 자연어 SAFETY 주석에만 적혀 있던 것들이 기계가 읽는 형태로 옮겨 가기 시작한 것 — 널 결과 뒤에서 조용히 일어난 이 변화가 아마 더 오래갈 것입니다.

참고 자료

• Verifying the Rust Standard Library (Cook 등, NASA Formal Methods Symposium 2026, arXiv 2606.17374) — 캠페인 결과 논문. DOI 10.1007/978-3-032-28079-4_19
• Kani: A Model Checker for Rust (arXiv 2607.01504, 2026년 7월 1일 프리프린트) — 도구 논문. 산업 코드베이스 사례 연구와 11개 버그
• model-checking/verify-rust-std — 검증 저장소 — 챌린지 29개는 doc/src/challenges/에서 직접 확인 가능
• verify-rust-std PR 238 — VeriFast의 LinkedList 증명 (챌린지 5)
• Kani Rust Verifier — 도구 저장소
• cedar PR 1037 — contains_at_least_two의 잠복 버그 수정
• hifitime 이슈 475 — Kani 검증 중 발견, 하네스를 버그 동작에 맞춘 사례
• Kani가 검사하는 미정의 동작 목록 — 무엇을 검사하지 않는지 확인용