Anthropic、123個のOSSを検証 1回に1億トークン超かかる

123のOSSをClaudeで形式的検証　証明は条件つきだ

AnthropicはClaudeを使ってソフトウェアにバグがないことを数学で証明する手法を開発し、123個のオープンソースライブラリで試した。組んだ相手は研究組織のTheoremだ。証明の途中で見つかったバグはClaudeで直し、直し続けた末にクラッシュが起きないことを証明できたという。

形式的検証は、コードを数式の形に置き換えてバグがないことを示す手法だ。考え方は昔からあるが、証明に手間がかかりすぎる。そのため使われてきたのは飛行機の航空電子機器のような、壊れると命に関わるシステムに限られていた。

背景にはAIでバグが大量に見つかる流れがある。PHPの緊急アップデートのように影響の大きい例も出ている。Anthropicは10月にもOSSの穴を探す取り組みを出しており、今回は見つける側から「無いと示す」側へ一歩進めた形だ。

証明できたのはRISC-VとLinuxの条件だけ　Armやx86は別だ

証明が成り立つ条件ははっきり絞られている。RISC-VのCPUとLinuxを積んだマシンで、メモリの量を固定し、単一スレッドの静的バイナリとして動かす場合だ。

Anthropic自身も限界を認めている。RISC-Vで問題がないと示せても、Armやx86ではバグが出る可能性が残る。実際に使う環境で無いと言い切るには、そのプログラムが動くすべてのマシン構成を網羅して表す必要があるという。

検証には1億トークン超　日本の開発現場が見るべき所

いちばん重いのは費用だ。形式的検証を1回走らせるのに1億トークン以上を使う。Anthropicは36件の検証でトークン量を並べ、Claude Opus 5.5がClaude Opus 5より少ない量で証明を終えたと示した。

Anthropicの見立ては2つある。モデルが賢くなれば使うトークンは減る。似た証明の手順は別のソフトでも使い回せる。この2つで費用の問題は少しずつ軽くなるとみている。

日本の会社で業務アプリを抱える人にとって、すぐ自社のシステムに使える話ではない。社内の業務アプリはクラウドのx86やArmのサーバーで動くことが多く、今回の条件とは合わない。まず効いてくるのは、自社が使っているOSSのライブラリが証明済みになるかどうかのほうだ。

OSSなら0円で申し込める　必要なのは3つのファイル

TheoremはLLMを使った形式的検証を、OSSのプロジェクトに無料で提供している。証明に使ったClaudeのスキルもGitHubで無料で公開された。

編集部が10月23日に「OSS Verify」の公式ページを開いて確かめた。無料になるのは条件を満たすOSSだけで、OSSでないソフトは個別の相談になる。申し込みはGitHubへのプルリクエストで、設定ファイル・Dockerfile・ビルド用のスクリプトの3つを出す。

• ビルドはRISC-V向けの静的バイナリに直す必要がある
• 証明の中身は64MiBまでの入力でクラッシュしないこと
• 見つかったバグは公開前に非公開で知らされる
• スキルの説明には、AIの指摘や修正案は間違うことがあり人が見る約束はないと書かれている

自社のサービスがOSSのライブラリに頼っているなら、その開発元がOSS Verifyに入ったかを追っておきたい。証明済みの部品が増えれば、脆弱性の対応に追われる回数そのものが減る可能性がある。