暗号化メッセージングの安全性は、見た目の便利さよりもずっと地味なところで決まります。Google DeepMind が今回発表したのは、AI エージェントを使って Signal の暗号プロトコル実装を形式手法で検証した、という話です。派手な新機能ではありませんが、ソフトウェアの安全性をどこまで機械的に保証できるのかという点で、かなり重い一歩だと思います。しかも対象が理論上の設計図ではなく、実際に動くコードだというのが肝です。
DeepMind の発表の中心は、AlphaProof Code という新しい agentic framework です。これは、人間の専門家と複数の AI エージェントが役割分担しながら、コードが満たすべき性質を数学的に証明していく仕組みだと説明されています。今回の対象は Signal の暗号プロトコルで、Signal アプリや Google Messages のようなサービスで使われている、私的な会話を守る技術です。
同社によると、研究者たちはまず、Signal のセキュリティ目標を formal mathematical specifications に落とし込みました。つまり、「何が安全なのか」を人間が解釈できる形ではなく、Lean という証明用の言語で扱える形にしたわけです。この段階では人間の専門家が一つひとつ確認しています。そこから先は Gemini Carbon を使ったエージェントが証明を進め、Lean のコードを 600 万行以上生成したとされています。Lean は、書かれた証明が数学的に正しいかを機械が検査するための言語です。
この仕組みが面白いのは、AI が勝手に全部をやるのではなく、証明の流れを研究チームの分業に寄せている点です。AI が証明候補を大量に作り、別の AI がそれを監査し、人間はそのうち 1% だけを重点的に確認する。残りは Lean が自動でチェックするので、人間は本当に判断が必要な場所に集中できる、という構図です。DeepMind は、このやり方で大規模なコードベースのうち人手で見る必要がある範囲を大幅に圧縮できたと述べています。
今回の検証は、暗号プロトコルの実装そのものまで踏み込んでいる点でも強調されています。これまでの形式検証は、設計レベルの分析で止まることが多かった一方、今回の手法はコンパイル後に実際に端末で動くコードが、指定したセキュリティ性質を満たすかを示したとしています。しかも、その性質には「端末が一時的に侵害された前後でもメッセージを守る」といった条件が含まれます。DeepMind は、この検証が 4 週間で完了したとも説明しており、歴史的には専門チームで数年かかる作業だと位置づけています。
さらに、AlphaProof Code がバグを見分けられるかを確認するため、既に修正済みの実際のバグを 2 件、隔離した Signal のコードに意図的に戻して試したそうです。その結果、どちらについても「そのバージョンは安全ではない」という機械検証済みの証明を出せたとしています。Signal 側の CTO である Ehren Kret 氏も、このアプローチが live code を valid Lean theorems に変換する点を大きな前進だと評価しています。DeepMind は関連資料をオープンソース化するとしており、技術論文も公開しています。
まず印象的なのは、DeepMind が売りにしているのがコード生成ではなく「証明」だということです。AI 開発の話はどうしても、「どれだけ速く書けるか」「どれだけバグを減らせるか」に寄りがちです。でもこの発表は、それよりもさらに厳しい基準を持ち出しています。ソフトウェアが正しいかどうかを、人間のレビューではなく、数学的に証明する。しかも対象は暗号通信の本丸です。ここは、AI を開発支援ツールとして見るのか、検証の実行主体として見るのかで、意味がかなり変わると思います。
ただし、ここで「AI がもう暗号を完全に理解した」と受け取るのは早いです。実際にやっているのは、あくまで形式化された条件のもとでの証明です。つまり、自然言語で「安全そうだ」と言うのではなく、「この仕様を満たす」と機械が確認できる形に変換できた、という話です。ここには大きな価値がある一方で、仕様に含め忘れたリスクや、そもそも設計側の前提がずれていた場合までは救えません。私は、今回の発表は万能の安全保証というより、「検証可能な範囲をどこまで広げられるか」の実演だと見るべきだと思います。
DeepMind が強く押し出しているのが、4 週間という期間です。形式検証は、理論的には美しくても現場では重い作業として知られています。仕様を詰めるだけでも大変で、証明の穴を埋めるのに人手がかかる。そこを AI エージェントの分業で圧縮した、というのが今回のニュースの実際のインパクトでしょう。私はこの点に、AI が「人間を置き換える」というより、「人間の仕事のうち最も消耗する部分を削る」方向の価値を感じます。
とくに注目したいのは、人間がレビューしたのが 1% だけだった、という記述です。これは単純にすごい数字に見えますが、裏を返せば、残り 99% は Lean の機械チェックに寄せられる程度まで、問題を分解できたということでもあります。形式検証が広く使われない理由は、数学が難しいからだけではありません。作業の粒度が細かすぎて、実務に乗せにくいからです。今回の仕組みは、その「面倒さ」を AI がかなり削れた可能性を示しています。もしこれが再現性を持つなら、暗号だけでなく医療機器の firmware や電力網の software にも効く、という DeepMind の主張には筋があります。
Signal はもともと、プライバシーを強く打ち出してきたアプリです。だからこそ、こうした発表の舞台としても説得力があります。もし一般的なアプリや、外から見てそこまで安全性を売りにしていない製品だったら、「すごい技術を試しました」で終わっていたかもしれません。けれど Signal のように、通信の秘匿性そのものがブランドの核になっているサービスでは、実装の正しさをどこまで詰められるかが、信頼の根拠になります。
一方で、ここには少し慎重に見るべき点もあります。今回の発表は、Signal の「核心部分」を検証したとはいえ、プロダクト全体の安全性を保証したわけではありません。実際のサービスでは、OS、端末、ネットワーク、ユーザーの運用、周辺機能まで含めてリスクが生まれます。暗号プロトコルが正しくても、アプリの外側で崩れることはある。だから私は、今回の成果を「Signal が完全に安全になった証拠」とは見ません。ただ、少なくとも最も重要な中核について、これまでより強い機械的裏付けを持てた、という意味は大きいと思います。
この発表の先にあるのは、単純な自動化競争ではないはずです。本当に問われるのは、形式検証を AI で扱えるようにした結果、どの領域が変わるのか、という点です。暗号やインフラの世界では、「速く作る」より「壊れていないと証明する」ほうが重要な場面がある。そこに AI が入ると、開発の主役はコードを書く人から、仕様を切り出し、証明の境界を設計する人へ少しずつ移っていくのではないかと思います。
ただ、そこには新しい難しさもあります。AI が証明を作れるなら、逆にその証明をどう監査するのか、どこまで結果を信じてよいのか、という問題が残ります。今回のように Lean が検査を担う構造は、少なくとも「AI の出力をそのまま信用する」話ではありません。私はここに、DeepMind の発表の健全さも感じます。誇張して「AI が安全を保証した」とは言わず、機械検証の枠にちゃんと戻しているからです。その意味で今回のニュースは、AI 安全の物語というより、検証可能性を実務へ押し戻す試みとして読むほうが正確だと思います。
参考: Formal Verification of Signal’s Protocol with Gemini — Google DeepMind
