DeepMind「AlphaProof Code」、Signalの暗号コードをコンパイル後の機械コードまで証明。Lean 600万行超を4週間で

まず初めに

「AIが暗号の正しさを証明した」という見出しは、盛る気になればいくらでも盛れる。だからこそ先に線を引く。この成果がすごいのは「AIが賢い」からではなく、設計図ではなく実際に動くコード、そのまた下の機械コードまで証明の対象を降ろした点にある。バグが潜むのはいつも設計と実装の隙間だ。その隙間に証明を持ち込んだ、という話として読むのが正しい。 ※個人の感想です

何が発表されたのか

Google DeepMindは2026年11月10日、Pushmeet Kohli氏とSwarat Chaudhuri氏による公式ブログで「AlphaProof Code」を発表しました。同社によれば、これは人間の専門知識とAIエージェントを組み合わせた、形式検証のためのエージェント型の枠組みです。形式検証とは、コードが仕様どおりに動くことを数学的に証明する手法で、同社は「セキュリティ保証の最高水準」と位置づけています。

今回の検証対象は、メッセージアプリSignalやGoogle Messagesなどで使われるSignalプロトコルの基盤コードです。同社は、広く展開されている暗号プロトコルについて、AIを使ってこの深さで形式検証したのは初めてであり、AIの有無を問わず、広く展開されたプロトコルの実装をこの深さで形式検証したのも初めてだとしています。

検証の進め方――人間は仕様、エージェントは証明

同社の説明では、AlphaProof Codeは複数の大規模言語モデルを使うエージェント型の枠組みで、研究チームの分業をまねた形になっています。まず研究者が複数のモデルと協力して、Signalのセキュリティ目標を形式的な数学の仕様へ翻訳し、人間の専門家がその全てを審査します。その後、Gemini Carbonで動くエージェントが証明を進め、Leanという証明支援言語で600万行を超える証明を生成しました。

エージェントは証明の監査も行い、人間が再確認すべき箇所を提示しました。その割合はコードベースの約1%にとどまったと同社は説明しています。残りはLeanが自動で検査するため、人間の専門家は判断が要る場所に集中できた、というのが同社の主張です。

証明が届いたのは設計の層だけではありません。同社によれば、エージェントはコンパイルされたコードが主要なセキュリティ特性を満たすことを、端末上で実際に動くコードの水準まで証明しました。特性の例として、一時的に端末が侵害された前後でもメッセージが保護されることが挙げられています。この複雑さでも検証は4週間で終わり、歴史的には専門家チームで数年かかる作業だったと同社は述べています。

対象の範囲――技術論文が示す線引き

技術論文側の記述によれば、検証の対象はlibsignalのバージョン0.105.4と、耐量子の仕組みに関わるspqrバージョン1.6.0を組み合わせたもので、通常のRustコンパイラでAArch64向けにコンパイルした実行ファイルです。対象となったのは、後方秘匿性（forward secrecy）、侵害後のセキュリティ（post-compromise security）、認証、ハンドシェイクの秘匿性といった特性で、セッションは1対1のものが対象です。証明の規模は注釈などを含めて約650万行という数え方も論文側で示されています。

つまり、証明されたのはSignalの全機能ではなく、暗号の中核にある一部のコンポーネントと、その主要特性です。グループ通話やアプリ全体の挙動まで証明されたわけではありません。この範囲の限定は成果を小さくするものではなく、証明という言葉を正確に使うための前提です。

検証系の信頼の土台についても、論文側は仕様と機械語の意味定義が中心であることを示しています。何を「正しい」と定義したか自体は人間が書いた仕様に依存するため、仕様の審査が工程の要になるという構造です。エージェントの証明をLeanのカーネルが検査する仕組みと合わせ、信頼の置きどころが明示されています。

正しさと間違いの見分け――バグを戻す試験

同社は、枠組みが正しいコードとバグのあるコードを見分けられるかを確認するため、過去に実際に修正された2件のバグを、隔離したSignalのコードへ意図的に再導入しました。どちらの場合も、システムはバグのある版が安全でないことを機械的に検査可能な形で証明したとしています。

発表にはSignalの最高技術責任者であるEhren Kret氏のコメントも掲載されています。同氏は、稼働中のコードを有効なLeanの定理へ自動で翻訳するエージェントの活用は大きな前進であり、AIによるセキュリティ脅威が増す中で、中核プロトコルの厳密な検証がプライバシー保証への信頼を高めると述べています。

同社は、形式検証の成果物（artifact）をオープンソースとして公開し、コミュニティが利用できるようにしたとしています。今後の応用先としては、医療機器のファームウェアや電力網のソフトウェアなどが例示され、防御側のエージェントであるCodeMenderと組み合わせる方向も示されています。形式検証でエージェントの証明能力を競う動きは、GoogleのAntigravity「/teamwork」が数学の予想をLeanで形式化した事例でも見られます。

IT Postの見方

IT Postでは、本件の要点は「証明の単価が下がり始めた」ことにあると考えます。形式検証はこれまで、正しさの保証としては最強でも、費用と期間の重さで適用範囲が極端に限られてきた。そこにエージェントが入り、数年が4週間になったというのが同社の主張です。数字は同社公表値として割り引いても、方向そのものは業界の前提を動かします。

一方で、証明は仕様の正しさを保証しません。「何を証明するか」を決めるのは人間で、今回も仕様の翻訳と審査に人間の専門家が全面的に入っています。証明が安くなるほど、ボトルネックは「正しい仕様を書けるか」へ移る。AIが証明を書く時代の希少資源は、証明ではなく仕様のほうだ、というのがこの発表の裏側の教訓です。

今後どうなりそうか

今後の確認点は、第一に公開された成果物を第三者がどこまで再検証するか、第二に対象範囲がlibsignalの他の部分や他のプロトコルへ広がるか、第三に医療機器や電力網といった例示分野で実際に適用が進むかです。枠組み自体の一般提供や料金は発表されていません。

新しい公式情報が確認できれば、続報として整理します。