필사 모드: Rust標準ライブラリ検証キャンペーンが見つけたメモリ安全性バグは0件だった

• はじめに — 史上最大というふれこみの検証キャンペーンの結果
• 何を検証しようとしたのか
• キャンペーンの構造 — 賞金付きのオープンコンテスト
• 数字 — 33,955個の関数のうちどこまで進んだか
• 実際に見つけたもの — 表2に記された4行
• null結果をどう読むか
• 対照群 — 同じツールが別のコードベースでは
  • 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所属の人々が名を連ねています。著者たちの表現で「ソフトウェアライブラリを対象に報告されたものの中で最大の検証キャンペーン」(著者自身の評価です)の結論が、「新たに見つかったメモリ安全性の脆弱性なし」なのです。

これは失敗談ではありません。そして成功談でもありません。形式検証が実務で実際にどんな価値を持つのかについて、広報資料よりはるかに有用なデータです。本稿はその数字をそのまま読んでみようと思います。

何を検証しようとしたのか

Rustの所有権型システムは、データレースとかなりの数のメモリエラーをコンパイル時に防ぎます。問題は、標準ライブラリ自身がunsafeコードに大きく依存している点です。コンパイラが検査しない5つの操作 — 生ポインタの参照外し、unsafe関数の呼び出し、可変staticへのアクセス、unsafeトレイトの実装、unionフィールドへのアクセス — の健全性は、結局のところ開発者の推論に懸かっており、その推論はたいてい自然言語のSAFETYコメントにしか記録されていません。

論文が引用する規模感はこうです。過去3年間にI-unsoundラベルで報告された健全性バグは74件を超え、これまでにCVEは18件登録されています(いずれも2026年3月時点)。Rustがカーネル・ブラウザエンジン・暗号ライブラリに組み込まれる今、この基盤を機械検証された証明で支えようというのがキャンペーンの動機です。

ここで用語を正確にしておく必要があります。このキャンペーンが目標とするのは未定義動作(UB)の不在 であって、完全な正確性ではありません。UBの不在はメモリ安全性の十分条件ですが、機能的正確性・ライブネス・セキュリティ特性までは保証しません。

キャンペーンの構造 — 賞金付きのオープンコンテスト

標準ライブラリは一つのチームが検証するには大きすぎます。そこでRust Foundationが運営するオープンコンテスト として設計されました。

検証課題はチャレンジ(challenge)単位に分割されます。各チャレンジは具体的な検証対象、前提条件のリスト、明確な成功基準、そして完了時に支払われる賞金を定義します。参加者がフォークしてPRを出すと技術レビュー委員会がレビューし、承認されればmodel-checking/verify-rust-stdフォークにマージされます。論文の基準(2026年3月)で、チャレンジ29件が公開されており、少なくとも4つの機関に所属する外部貢献者21名以上から、PR450件以上を受け取っています。

この数字はリポジトリで直接確認できます。doc/src/challenges/以下に0001-core-transmutation.mdから0029-boxed.mdまで正確に29件があり、リポジトリは今も生きています。

コンテストはツール中立です。Rust標準ライブラリで動作し、CIに統合され、(通常は査読付き論文に裏付けられた)明確な健全性保証を提供すれば、どんなツールでも受け入れられます。現在サポートされているツールは4つです。

• Kani — CBMCベースの有界モデル検査。キャンペーンの主力。
• ESBMC — こちらもモデル検査。
• Flux — 精緻型(refinement type)で数値範囲と安全性の事前条件を検査。
• VeriFast — 分離論理(separation logic)。対象とする関数に限り、ポインタのエイリアシング違反を含むすべてのUBの不在を検証。

Verus、Creusot、KRust、RAPxの4つはレビュー中です。論文が強調するのは、この多様性が好みの問題ではなく必然だという点です — アーキテクチャ固有のイントリンシック、ポインタ中心のコード、並行処理プリミティブ、複雑な不変条件を持つループは、それぞれ異なる推論技法を要求します。単一のツールではすべての検証条件を消化できません。

数字 — 33,955個の関数のうちどこまで進んだか

nightly-2025-10-08ツールチェーンのスナップショット基準で、core・alloc・stdの3クレートには関数が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に記された4行

つまり、このすべての作業が見つけたイシュー全体が表2です。

4行です。そしてこのうち3つはコードバグではなく仕様とドキュメントの問題 です — 欠落した安全性表記、誤ったSAFETYコメント、関数の動作を誤って記述したドキュメント。

論文はこれを副次的な利得として正直に位置付けています。形式仕様を書くという行為自体が、自然言語コメントだけでは出てこない安全性要件の精密な表現を強制するということです。実際にこの効果はRust言語自体に痕跡を残しました — 言語チームが契約(contract)を実験的な言語機能として採用し、Rustプロジェクトは標準ライブラリに安全性契約を付ける公式目標を採択しました。

ところが唯一のコードバグである最初の行、「誤ったSIMDシフト結果」には反転があります。論文の第7節が直接明かしています — チャレンジ15はSIMDイントリンシック565個の実行可能モデルに対するランダムテスト で完了したのであって、形式証明で完了したのではありません。再現のためシードをログに記録し、アップストリームのバグ2件を見つけましたが、著者たちの表現ではこれは「形式検証ではなく高信頼度の検証(validation)」として読むべきだとされています。

まとめるとこうなります。史上最大規模の検証キャンペーンが標準ライブラリで見つけたコードバグは、形式検証ではなくランダムテストが見つけたものでした。

null結果をどう読むか

論文自身の解釈から見ていきます。

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.

つまり「形式検証は無用だ」ではなく、「Rust標準ライブラリの既存テストがすでに非常に優れている」というシグナルとして読みます。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はプロダクションのrustコードベース4か所で、テストとファジングが見逃したバグ11件 を見つけました。

同じツール、正反対の結果です。違いはツールではなく対象コードの既存テストの成熟度 です。

try_fit — 1,677万回のファジングが超えられなかった壁を20秒で

最も印象的な事例です。s2n-quicはAmazonの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のシンボリック実行はそこへ直行します。

2つ目のs2n-quicの事例は逆に相補性を示します。decode_packet_numberバグはKaniが2.8秒で、ファジングが1分以内に、それぞれ独立に見つけました。両方が見つけた場合でも、Kani側のほうがより実行可能な情報を与えます — 正体不明のクラッシュではなく名前の付いた性質の失敗を指し示し、concrete playback機能によって開発者が普通のRustテストとして再生できる具体的な反例を生成します。

テストが原理的に見られないもの — Firecracker

FirecrackerはAWS LambdaとFargateの背後にあるVMMです。Kaniをセキュリティ上重要な2つのコンポーネントに使っています。

I/Oレートリミッタはトークンバケットです。関心のある性質は「マイクロVMがどの1秒区間でも設定されたI/O帯域幅を超えられない」というものです。ところがこれは本質的に時間依存です — 補充されるトークン数がauto_replenishがシステムクロックに対していつ呼ばれるかに懸かっており、漏れなくテストするのは不可能です。

Kaniの解決策は、libc::clock_gettimeを単調非減少のInstantを返す非決定的なスタブに差し替えることです。時間の次元そのものをシンボリック変数に変えてしまいます。こうして作られたハーネスがレートリミッタで複数のバグを見つけ、最も重要だったのは、敵対的にタイミングを合わせた呼び出しでゲストが自身のI/O予算を最大0.01%まで超過できてしまう丸め誤差でした。

ここで正直に触れておくべきことがあります。0.01%は実務上とても小さな超過です。これを「致命的な脆弱性」として演出すれば嘘になります。興味深いのは大きさではなく種類 です — この誤差は補充呼び出しがシステムクロックに対してミリ秒未満のレベルで正確にいつ起きるかに懸かっており、これはテストが決定論的に制御できず、ファジングも明示的な時間モデルなしには狙えない条件です。

2つ目はVirtIOデバイスエミュレーションです。ホストとゲストが共有するメモリは敵対的な攻撃面です — 信頼できないゲストが共有ディスクリプタとリングバッファに任意の値を書き込める可能性があります。Kaniは非決定的なゲストメモリでこのシナリオを表現し、VirtIO仕様2.6.7.2節への準拠を検証したうえで、ゲストがVirtIOキューコンポーネントの開始アドレスをMMIOギャップに置くことでFirecrackerを起動中にpanicさせられるというバグを追加で見つけました。

Cedar — 形式参照モデルさえ防げなかったもの

Cedarはオープンソースの認可ポリシー言語かつエンジンです。この事例が特別なのは、Cedarがすでに形式参照モデルに対する差分テストを行っていた という点です。それでもバグはプロダクションコードまで生き残りました。

contains_at_least_twoは文字列に特定の部分文字列が2回以上出現するかを検査します。マルチバイト文字を検索語として渡すと、&strを文字境界でない位置で切ってしまうことがあり、ランタイムpanicが発生します。既存のテストすべてで沈黙していました。Kaniのシンボリック実行が反例を作り、修正はcedar PR 1037としてマージされました(2024年7月)。

日付に注意してください。Kani論文は2026年ですが、個々の事例の年代はまちまちです — Cedarの修正は2024年のものです。論文が2026年にこれらの事例をまとめて報告しているのであって、11件すべてが2026年に見つかったわけではありません。

契約が開いた扉 — そしてバグを肯定していたテスト

Hifitimeは高精度時刻管理ライブラリで、FireflyのBlue Ghost Mission 1月着陸ミッションに使われました。ここがKani論文の契約(contract)事例研究です。

Kaniの契約は、関数の事前条件・事後条件・ループ不変条件をRustのブール式で書きます。これがなぜ重要かというと、有界モデル検査を無界 保証へ引き上げるからです — ループを漏れなく展開する代わりに、不変条件が帰納的であることを検証し、それでループを抽象化します。論文の表現では、第1段階は演算がクラッシュしないことを証明し、第2段階は演算が正しく計算する ことを証明します。

機能的性質を確立する副次効果として、Kaniは以前知られていなかったバグ6件を見つけました。panic不在ハーネスでは表現すらできなかった性質です。最も意味のある2つは、Rust標準ライブラリ自身の要求に違反していたものでした。

• EpochのPartialEq/Ordの不整合。 Duration::PartialEqは符号が逆の値を意図的に等しいとみなします(向きと無関係な区間長を表すからです)。ところがEpoch::PartialEqはこの実装に委譲していた一方、Epoch::Ordは符号を区別する辞書式比較を使っていました。Rust標準ライブラリはa == bならばa.cmp(b)がOrdering::Equalでなければならないと要求します。符号が異なるすべてのエポックの組でこの不変条件が破られていました。
• DurationのPartialEq/Ordの不整合(ゼロ交差)。 根は同じです。2つのDurationがa == bとa < bを同時に満たすことがありました。

Epochバグがなぜテストで捕まらなかったのかが、この記事の要点を凝縮しています — どのテストもエポックをその符号反転と比較していなかったから です。「時点」について概念的に奇妙な演算だからです。Kaniのシンボリック実行は、あらゆる可能なEpochの組を探索しながら、この入力を自動的に作り出しました。

そして最も痛いディテール。total_nanoseconds()の符号誤り(負の方向に1世紀を超える期間で、加算の代わりに減算を使っていた)を契約が捉えたとき、修正はソース1文字でした。ところが既存の統合テストの一つが、そのバグの挙動を正しいとアサーションしており、実装と一緒に直す必要がありました。論文の診断は鋭いです — テストオラクルが実装の出力を見て書かれていたため、同じ誤りをそのままエンコードしていたのです。事後条件はDuration型のエンコーディング不変条件から導かれていたため、実装とテストの両方を独立に検査できました。

この罠は論文の外でも確認できます。Hifitimeリポジトリのイシュー475は、Kani検証作業(PR 474、2026年4月マージ)中に見つかったtry_truncated_nanosecondsのエラー分類バグですが、イシュー本文にはこう書かれています — 「証明が通るよう、Kaniハーネスを現在の(誤った)挙動に合わせて更新した。実際の実装は別途修正が必要」。仕様を実装に合わせれば、検証は通りバグは残ります。検証ツールがあっても、人間が仕様をどこから持ってくるかがなお全てです。

LLMが仕様を書くとき — 測定された結果

Hifitimeの第2段階仕様は、シェルアクセス権限を持つAIコーディングアシスタントで開発されました。ワークフローはタイトなループでした — アシスタントが契約アノテーションを提案し、ソースに書き込み、cargo kaniを実行し、結果(成功/失敗/タイムアウト/コンパイルエラー)を観察し、仕様を練り直します。人間の研究者はどの関数を狙うかを指示し、ドメインの文脈を与え、提案された契約の妥当性をレビューしました。

Kaniの仕様言語がRustの拡張であるという点が、ここで有利に働きます。契約がRustのブール式であり、ハーネスがRust関数であるため、アシスタントは別の形式言語を学ぶことなく既存のRustの知識をそのまま使います。

論文が強調するのは結果よりも構造です。

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

つまり仕様を信頼する必要がないということです。実際、AIが生成した契約3件が検証に失敗し、Kaniが3件とも捕まえました。

1. 検証対象の関数を自分自身のensures節から呼び出す、手に負えない事後条件 — SAT式が2倍になりソルバーがタイムアウトした。(アシスタントが直接的な算術式に単純化)
2. 広すぎるシンボリック入力(kani::any::<Epoch>())がTimeScale::ETバリアントを含んでしまい、sin()をSAT式に引き込んでタイムアウトした。(TimeScale::TAIに制限)
3. const fn非互換 — Kaniのマクロ展開がnon-constコードを生成し、コンパイルエラーになった。(独立した証明ハーネスに切り替え)

分類すると、仕様設計の誤りが1つ、ハーネス設計の誤りが1つ、Kani自体の限界が1つです。3つともアシスタントが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はRustリファレンスが列挙するUBの部分集合しか検査しません。検査していない ものが軽視できない量あります。

• ポインタエイリアシングモデル(Stacked Borrows / Tree Borrows)違反
• データレース
• 誤ったインラインアセンブリ
• プロブナンス関連UBの一部の形態
• unsafe境界をまたぐ型安全性不変条件の保存(例:Vecの長さが容量を超えないこと)

論文の文章そのままに — 現在のすべての検査を通過した関数も、より完全なモデルの下ではなおUBを示しうるとされています。

仕様とモデルの空白。 Rustにはまだ批准された形式仕様がありません。 エイリアシングモデルのような中核部分には競合する提案があり、将来仕様が変われば、今日の前提の下で健全だった証明が無効になる可能性があります。イントリンシックや外部関数を呼び出す関数の検証は、その演算に提供されたモデルの忠実度に依存し、モデルが不正確であれば健全でない検証結果が生じる可能性があります。

ツールチェーンの健全性。 すべての結果はツール自体の正しさに依存します — KaniのMIR-to-GOTO変換、CBMC、呼び出されるSAT/SMTソルバー、VeriFastのシンボリック実行エンジン。論文が直接書いています。これらのツールのどれ一つとして、それ自身が形式検証されてはいません。 信頼性は広範なテストとファジング、そして数年間のプロダクション使用に依存しています。

並行処理はまるごと空白です。 29個のチャレンジのうち2つが並行処理APIを狙っています — チャレンジ7(atomic型)とチャレンジ27(Arc)。どちらも承認された解答が一つもありません。 unsafe Rustにおけるデータレースは即座にUBであるにもかかわらずです。難しいのは、緩和メモリモデルの下でロックフリーなデータ構造を仕様化し検証することです。

残っている領域。 1万個を超える関数を検証しましたが、標準ライブラリは完全な検証には程遠い状態です。BTreeMapの内部、atomic型、String、イテレータ、ベクタ、デック、参照カウント型など、影響力の大きいAPIの多くが部分的にしか扱われていないか、まだ手つかずです。

Kani論文も自らの事例研究の偏りを認めています — 評価対象のプロジェクトはランダムな標本ではなく自らKaniを採用した場所 であり、有利な事例が過大に代表されている可能性があります。Cedarの実験がKaniを使っていなかったプロジェクトに対する意図的な評価であるため、これを部分的に緩和すると書かれています。

コスト

証明の保守。 検証リポジトリはアップストリームのrust-lang/rustのフォークであり、定期的に同期する必要があります。ところがRustは6週間ごとに新リリースを出します。 論文の結論は、この方式が持続可能であるためには、契約と証明をアップストリームに上げて、証明の保守が標準的な開発ワークフローの一部にならなければならないというものです。今はそうなっていません。

コンパイル時間。 ハーネスが急増するにつれ、コンパイルがボトルネックになりました。専用のコンパイラベンチマークツールを作り、並列化・キャッシュ・ヒューリスティックなコード生成順序・関数のスタビングを組み込んで、標準ライブラリのコンパイルで3.97倍の速度向上を得ました(著者自身の測定、素朴な逐次パイプラインとの比較)。

CI時間。 Kani論文の表1に基づきます。

大半は25分以内に終わります。PRワークフローに組み込める予算だというのが論文の主張であり、この表を見ると納得できます。ただし、ハーネス数と時間が線形ではないことも見て取れます — ハーネス1個のrust-sel4が4分、10個のzerocopyが3分です。ハーネスの個数よりも個々の証明の難易度が支配的です。

人と組織のコスト。 論文の5.1節が最も率直です。初期の計画は技術的なマイルストーンに集中しており、コミュニティの合意形成と機関間の調整にかかる時間を大きく過小に見積もっていた と認めています。契約をRustコンパイラに統合するには、言語チーム・ライブラリメンテナ・ツール作者からの広範な支持が必要で、技術的には単純な変更でさえ、関係者を早期に巻き込まなければ止まってしまいました。外部機関との協業には数か月かかる法的合意 が必要でした。外部貢献者を引き込むにも賞金だけでは足りず、難易度のスペクトラム、明確なドキュメント、動くサンプルが必要でした。

ツールごとのオーバーヘッド。 VeriFastでLinkedListを証明したPR 238(チャレンジ5、2025年8月マージ)がこのコストをよく示しています。関数19個を直接検証し、5個の健全性を含意しますが、VeriFastはゴースト命令を入れるためにソースを少し書き換える必要があります(例:forループをloopに、Option::mapを1階の等価物に)。そのためCIパイプラインは3段階です — VeriFastが注釈付きコードを検査し、精緻化チェッカー が元のすべての振る舞いが注釈版の振る舞いでもあることを機械的に検証し、diffが元のコードがアップストリームと一致するかを確認します。モデル検査に比べて演繹的検証が課すエンジニアリング負担をそのまま示すと同時に、より深い保証(すべてのUBの不在)を得る代償でもあります。

では、いつ使い、いつ使わないべきか

2つの論文を重ねると、判断基準がかなり鮮明に見えてきます。

値をなす場合

• 既存のテストが原理的に届かない性質がある。 時間依存のコード(Firecrackerのレートリミッタ)、敵対的入力が入ってくる共有メモリ境界(VirtIO)、エンコーディング境界のような疎な入力領域(try_fit)。ファジングに勾配がない場所こそ、シンボリック実行の出番です。
• コードが狭く、状態空間が明確である。 表1でCIが短いプロジェクトに共通する特徴です。
• 性質を仕様として書ける。 Eq/Ordの一貫性、エンコード-デコードの往復一致のように、実装と独立に導ける不変条件があれば、契約は本当の価値を発揮します。Hifitimeの事例がこれを示しています。
• 回帰を防ぐことが目的である。 すでによくテストされたコードであっても、CIに常駐する機械検査済みの証明は今後の回帰を捉えます。標準ライブラリキャンペーンが実際に生きている点です。
• すでにプロパティテストがある。 s2n-quicのようにBoleroを使っていれば、属性一つで同じハーネスが証明になります。限界費用がほぼゼロです。

過剰であるか、まだ機が熟していない場合

• コードがすでにMiri級で検証されている。 標準ライブラリの結果がまさにこのケースです。新しいバグを期待して入っていくとがっかりします。
• ジェネリクスがコードの中心である。 Autoharnessがスキップした関数の56%がジェネリックです。Rustはコンパイル時に単相化するため、未インスタンス化の型パラメータの入力を合成できません。
• 並行処理が核心である。 チャレンジ7と27に承認された解答がないという事実が、現在の成熟度を物語っています。緩和メモリの下でのロックフリーデータ構造はまだ未解決の問題です。
• エイリアシング・データレースが主なリスクである。 Kaniはこれを見ません。この領域は依然としてMiriの担当です。
• 仕様を実装からコピーしてこようとしている。 イシュー475と上記のHifitimeのバグが示すように、実装を見て書いた仕様は実装のバグをそのままエンコードします。これでは検証は通り、バグは残ります。独立に導ける仕様がなければ、検証は高価な同語反復です。

一文にまとめるとこうです。形式検証の価値は、ツールの強力さではなく、あなたの既存テストが届かない領域がどれだけ広いかに比例します。

おわりに

この2つの論文が一緒に読まれるべき理由がここにあります。片方だけ読むと、間違った結論になります。

NFM論文だけを読むと、「史上最大の検証キャンペーンがバグを0件見つけた — 形式検証は過大評価されている」になります。Kani論文だけを読むと、「1,677万回のファジングが見逃したものを20秒で見つけた — なぜまだ使っていないのか」になります。どちらも同じツール、同じチームの結果です。

本当の結論はその間にあります。標準ライブラリでバグが出なかったのは、ツールが弱いからではなく、対象がすでに何年もMiriとテストで鍛えられていたからであり、s2n-quicとHifitimeでバグが出たのは、ツールが魔法だからではなく、そのコードにテストが原理的に届かない隅があったからです。形式検証はテストの上位互換ではなく、テストと相補的な、別の形をした網 です。

そして最後に、このキャンペーンが残した最大の資産は、証明11,970件ではないのかもしれません。契約がRustの実験的な言語機能になり、標準ライブラリに安全性契約を付けることがプロジェクトの公式目標になりました。自然言語のSAFETYコメントにしか書かれていなかったものが、機械可読な形へと移り始めたこと — null結果の裏で静かに起きたこの変化のほうが、おそらく長く残るでしょう。

参考資料

• 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が検査する未定義動作の一覧 — 何を検査していないかの確認用