Microsoft Researchは2026年11月5日(現地時間)、AIエージェントが生成するコードの形式検証を支援するツールキット「PDD Kit」を発表した。PDD Kitは、開発者の意図を形式仕様に変換し、エージェント生成コードがその仕様をあらゆる入力に対して満たすことを証明する。証明が現実的でない箇所ではテストにフォールバックする仕組みを持つ。これにより、開発者はコードの全行レビューではなく、当初の意図のレビューに集中できるとされている。
PDD Kitは、形式手法を専門知識を持たないエンジニアや日常的なアプリケーションにも適用することを目指している。AIエージェントが生成するコード量が大規模化する中で、人間による逐次レビューのスケーリングが困難になる問題に対処する。
従来の開発プロセスでは、エージェントが開発者の意図する計画から逸脱し、その実装に合わせたテストを生み出してしまうことで、バグが隠蔽される可能性があった。PDD Kitはこの課題に対し、開発者の意図をVerusの形式仕様に変換し、生成コードがその仕様を満たすことを数学的に証明することで、コード品質と信頼性の向上を図る。
同ツールキットは、GitHub Nextのリアルタイム共有開発環境「Chopin」と連携して機能する。開発チームは平易な言語で意図をレビューし、PDD Kitがこれを形式仕様またはテストに変換する。形式化可能な部分については、コードが導出された形式仕様を満たすことの証明が行われ、それ以外の部分に対しては高品質なテストが生成される。
検証の具体例として、Rustで記述されたフルスタックWebアプリ「Pet Store」のログインロジックにPDD Kitが適用された。この検証により、コードが強化され、既存のバグが発見されたという。開発者は意図のみをレビューし、生成されたコードを逐次確認することはなかった。
PDD Kitによる検証は、あらゆる入力に対するコードの仕様適合性を数学的に証明する「形式検証」と、コードを実行して動作を観察する「経験的検証」の二つの柱で構成される。形式検証にはMicrosoft Researchなどが共同開発したVerusが使用される。経験的検証はサードパーティの暗号ライブラリやユーザーインターフェースなど、証明が困難な領域をカバーする。これにより、PDD Kitは、人間が大規模なコードの安全性を検証するための信頼できる手段を提供することを目指している。
参考: Microsoft Research Blog (アーカイブ) — 2026年11月6日 01:00 (JST)