形式検証(formal verification)とは | プログラムが決めた仕様を必ず満たすことを数学で証明する方法と、AIで何が変わったか

意味

英語ではformal verification。形式手法と呼ばれる分野の一部です。手順はおおまかに三つに分かれます。

一つ目は、仕様を決めること。このプログラムにとって正しいとは何か、を数学の言葉で書きます。たとえば、どんな入力でも異常終了しない、圧縮して展開すると元に戻る、といったものです。二つ目は、プログラムを数学の模型に書き換えること。三つ目が、模型が仕様を必ず満たすことの証明を書き、証明支援の仕組み(RocqやLeanなど)に機械的に確かめさせることです。

証明できなければ、仕様を破るバグがありうるということで、失敗の仕方がバグの在りかを教えてくれます。それを直して繰り返すと、最後には、模型の上でその仕様に反する振る舞いが存在しない、という証明が得られます。

テストやファジングとの違い

テストは、用意した入力で試して、問題が起きなければ合格とするやり方です。ファジングは、大量の入力を機械的に作って試し続ける方法で、長く回すほど多くのバグが見つかります。ただしどちらも、試した範囲のことしか言えません。すべての経路を通ったという保証はない、と当サイトは理解しています。

形式検証は、ここが違います。条件を満たす入力のすべてについて、一度に議論します。だから、決めた仕様と条件の範囲内では、もう探すものがない、と言える。その代わり、議論そのものを書く手間が重くのしかかってきました。

なぜ広まらなかったのか、そして2026年10月に何が示されたか

証明は、元のコードより何倍も大きくなります。書くには特殊な技能も要ります。Anthropicが挙げる例では、あるOSの中核は、作るのに2人年、形式検証には20人年かかりました。そのため、航空機の制御のような、本当に失敗できない場面に限られてきた、と。

10月22日、AnthropicはTheoremと組み、Claudeに証明を書かせた研究を公表しました。オープンソースのライブラリ123本の239の入口について、64MB以下のどんな入力でも異常終了しないことを、決めた前提のもとで、機械語の水準で証明したとしています。証明は合計でおよそ1億8000万行。その過程で、何年も見つからなかったバグも数百件見つかりました(レビュー)。

量が増えても人が読む必要はありません。証明が仕様を満たしているかは、証明支援の仕組みが機械的に確かめるからです。人が信じなければならないのは、機械とOSの模型、証明したい主張の文、そして検査する仕組みそのもの、という整理になります。

見るべきところ

当サイトは、形式検証をうたう説明を見るとき、次の三つを合わせて見ることを勧めます。

何を証明したのか。異常終了しないことなのか、仕様どおりに動くことなのか。性質が書かれていなければ、保証の中身は分かりません。

どんな条件のもとでか。どの機械、どのOS、どんな入力の範囲か。条件が実際の使われ方とずれていれば、証明はその分だけ届きません。

何を信じることになるのか。模型と、主張の文と、検査する仕組みは信じるしかありません。形式検証済みという言葉は、バグがないという意味ではない、とAnthropicも明記しています。

関連する用語とレビュー

AIが証明を書く時代(レビュー) / 協調的開示とは / ゼロデイとは / AIの第三者評価とは / AI用語解説トップ

Anthropic「LLMs are making formal software verification feasible at a much larger scale」(2026-10-22)