コードが仕様どおりに動くことを数学的に証明する形式検証は、長らくセキュリティの最高水準とされながら、ほとんどの人には高すぎる手法でした。Anthropicは分かりやすい例を挙げています。seL4カーネルは開発に2人年、検証に20人年かかりました。Anthropicは検証専門企業Theoremとの共同作業で、Claudeが数年前には考えられなかった規模でこうした証明を作ったと報告しています。
鍵は、仕様を手で書かずに済ませたことです。チームはGoogleのOSS-Fuzzのファズテスト、つまりどんなクラッシュもバグとみなす小さなエントリーポイントを取り出し、それぞれを形式的な主張に変えました。コンパイル済みのRISC-Vバイナリは、64 MB未満のどんな入力でも、AddressSanitizerが検出するメモリ安全性のエラーを含めてクラッシュしない、というものです。数週間で、Claudeは123のライブラリにまたがる239のエントリーポイントでこれを証明し、途中で見つけたバグも修正しました。証明は主に証明支援系Rocqで書かれ、合計約1億8,000万行に上ります。典型的な証明は、命令数の中央値が18,000のバイナリに対して約600,000行です。人が読む必要はなく、Rocqの検証器が正しさを確認します。
すぐに得られた成果はバグです。いくつかは、ファザーではめったに見つからない種類のものでした。たとえば、ある展開処理での範囲外書き込みは、特定の構造をもつ約20 MBの入力でしか現れませんでした。別の実験では、LinuxカーネルのzlibをRFC 1950の形式版に照らして証明し、Pythonの一部を扱うRust製インタープリターを検 証して、170万個のランダムなプログラムの99.95%でCPythonと一致することを確かめました。コストも下がっています。36の小さな課題で、Claude Opus 5.5はOpus 5より約40%少ないトークンで半数を証明し、エージェント間で証明を共有すると17%節約できました。
ライブラリの保守担当者にとって、これは、ファジングがそうなったように、機械で検証された保証が一般的なライブラリで当たり前になりうることを示す、これまでで最も強い証拠です。Theoremは、ほかのオープンソースプロジェクトでもこの手順を実行すると申し出ており、Claudeのスキルも公開しました。
著者らは限界について慎重であり、読者もそうあるべきです。検証済みはバグがないことと同じではありません。証明の対象は、muslと静的にリンクしたシングルスレッドのRISC-Vビルドですが、多くの利用者はこれらのライブラリをx86やARM上でglibcとともに使っています。AddressSanitizerはすべてのメモリバグを検出するわけではなく、すべてのエントリーポイントを網羅したわけでもなく、呼び出し側がライブラリを誤用する可能性も残ります。証明に数億トークンかかりうることも、エコシステム全体に広げるうえでの本当の壁です。