0
会員（無料）になると、いいね！でマイページに保存できます。
共有する
アンソロピックは10月22日（現地時間）、パートナーのTheoremとともに、AIのClaudeでオープンソースのライブラリ123本が「クラッシュしない」ことをアセンブリ水準で形式検証したと発表した。証明は約1億8000万行に及び、作成の過程で数百件ものバグも見つかったという。
ClaudeによるOSSライブラリの形式検証を紹介するアンソロピックの研究ブログ
アンソロピックは10月22日（現地時間）、同社の研究ブログで、AIのClaudeを使い、オープンソースソフトウェア（OSS）のライブラリ123本について、入力が64MB未満であればクラッシュしないことを数学的に証明したと明らかにした。パートナーのTheoremと共同で取り組んだもので、コンパイル後のアセンブリ（機械語）の水準で、実際に使われているソフトウェアへAIによる形式検証を大規模に適用したのは初めてだとしている。
対象は、グーグルのファズテスト基盤「OSS-Fuzz」にある123のライブラリ、239のエントリポイント（テスト用の入り口）。ファズテストは、半ばランダムな入力を大量に与えてクラッシュを探す手法で、すべての入力を試せるわけではない。今回は、このテストを「どんな入力でもクラッシュしない」という仕様に自動で置き換え、Claudeが証明を書いた。証明が仕様を満たすかどうかは、証明検査系「Rocq」が機械的に確かめる。
作業は数週間で完了し、証明は約1億8000万行のRocqコードに上る。典型的な1件は約60万行で、対象バイナリの長さは中央値で1万8000命令だった。証明の過程で数百件のバグが見つかり、Claudeが自ら修正したうえで、修正後のコードを改めて証明した。libexpatの脆弱性CVE-2026-56132の再発見も含まれるという。
一方、アンソロピックは限界も明記している。証明は、単一スレッドで動く静的なRISC-VバイナリがLinux上で動くことなどを前提とし、「形式検証済み」は「バグなし」を意味しないと強調した。
同社は、証明の一部と、RISC-VおよびLinuxの形式モデルを公開した。Theoremは他のOSSプロジェクトにも同じ処理を実行すると申し出ており、開発者向けのClaudeスキルも公開するという。同社は20日にも、ClaudeでOSS25件の攻撃対象領域を分析し493件の問題を見つけた取り組みを公表していた。
では、なぜ兆回に及ぶテストをすり抜けたバグを、AIの証明は暴けたのか。背景には、AIが証明を通すために使いかねない「抜け道」と、証明1本あたりのコストをめぐる数字がある。
【画像解説と記事全文はこちら】ファザーが見逃しやすい、Claudeが見つけたバグ
ファザーが見逃しやすい、Claudeが見つけたバグ
（出典：アンソロピックの公表内容をもとに作成）
この記事の続き ＞＞
・ファザーが1MBで止まる間に潜んでいた、20MBと64MBのバグ
・AIが「クラッシュしないプログラム」に書き換える抜け道への対策
・証明に数億トークン、Opus 5.5で40％減というコストの現実
この続きは
会員限定（完全無料）です
ここから先は「ビジネス+IT」会員に登録された方のみ、ご覧いただけます。
今すぐビジネス＋IT会員に
ご登録ください。
今だけ毎月当たる！ずっと無料の会員登録キャンペーン
ビジネス＋ITプレミアム会員（無料）に登録すると
抽選で毎月20名様に
Amazonギフト券
5,000円分
当たる！
プレミアム会員に登録する（ずっと無料）
キャンペーン詳細・応募条件を見る
※この表示が出ている方は自動的にキャンペーンにエントリーされます。特典送付時にビジネス＋ITプレミアム会員を継続し、メールマガジン購読設定をオンにしていることが条件です。その他の条件は詳細をご覧ください
すべて無料！今日から使える、
仕事に役立つ情報満載！
ここでしか見られない
2万本超のオリジナル記事・動画・資料が見放題！
完全無料
登録料・月額料なし、完全無料で使い放題！
トレンドを聞いて学ぶ
年間1000本超の厳選セミナーに参加し放題！
興味関心のみ厳選
トピック（タグ）をフォローして自動収集！
AI・生成AIのおすすめコンテンツ
Googleで見つけやすく
評価する
いいね！でぜひ著者を応援してください
会員（無料）になると、いいね！でマイページに保存できます。
関連タグ