AnthropicとTheoremが、Claudeを用いて123のオープンソースライブラリにある239のテスト入口について、限定条件下でクラッシュしないことを形式的に証明。開発現場の品質保証を変える可能性と、その適用範囲を解説する。
30秒でわかる / THE SIGNAL
Claudeが生成した約1億8,000万行の形式証明を独立した証明チェッカーで検証。対象は123ライブラリの239のテスト入口で、64MB未満の入力や特定のRISC-V・Linux環境などの前提がある。ソフトウェア全体の完全な安全性を意味するものではない。
ソフトウェアの安全性は、どう確かめる？
私たちが日常的に使うアプリやWebサービス。その裏側では、開発者たちが膨大なテストを繰り返している。しかし、何百万回、何億回とテストを実施しても、すべての入力条件を試せるとは限らない。そこで注目されるのが「形式検証」だ。プログラムが定められた条件を満たすことを、数学的な方法で証明する技術である。従来は専門家による多大な作業が必要だったが、AIによって、そのハードルが下がり始めている。
Claudeが123のライブラリで実証
2026年10月22日、AnthropicはTheoremとの共同研究成果を発表した。Claudeを使い、123のオープンソースライブラリに含まれる239のファズテスト入口について、特定の条件下ではクラッシュしないことを証明したという。証明の総量は約1億8,000万行。作業の過程では、長年のテストで見つかっていなかった不具合も発見し、修正したと説明している。ここで重要なのは、AIの出した答えをそのまま信用しているわけではないことだ。Claudeが作成した証明は、Rocqという形式証明システムのチェッカーによって検証される。AIに作業を任せ、その成果を別の仕組みで確かめる。この構造は、今後のAI活用を考えるうえでも重要なポイントだ。
「すべて安全」という意味ではない
今回の成果には適用条件がある。研究の主な対象は、64MB未満の入力について、単一スレッドの静的バイナリ、固定メモリ予算、RISC-V CPUとLinux環境などの前提を置いたプログラムだ。証明されるのは、定義されたテスト入口と仕様に関する特定の性質であり、ライブラリ全体にあらゆる不具合が存在しないという意味ではない。実行が必ず終了することまで保証するものでもない。それでも、これまで専門家の大きな負担となっていた数学的な検証を、AIが大規模に支援できる可能性を示した点は重要だ。
WORK SIGNALの視点：AI時代は「検証する力」がさらに重要になる
AIによって、プログラムを作る速度は上がっている。しかし、作れる量が増えるほど、その品質をどう確認するかという課題も大きくなる。今回の研究は、AIが開発作業だけでなく、品質保証にも貢献できる可能性を示している。そして、もう一つ大切なのは、何を証明すべきかを定義することだ。AIがどれほど優秀でも、検証する条件が不十分なら、必要な安全性を確かめたことにはならない。これからの開発現場では、コードを書く技術に加え、要件を正確に定義し、AIの成果を検証する力がますます重要になるだろう。AIが仕事を速くするだけでなく、仕事の確かさを支える。そんな未来が、少しずつ具体的になってきている。