Microsoft Research· Alex Lavaee, Matthai Philipose·· 5 時間前厳選AI スコア65
Microsoft Research、形式検証でエージェント生成コードを保証する「PDD Kit」を発表
Formally verifying agent-written full-stack web apps with PDD Kit
AI ガイド
Microsoft ResearchはGitHub Nextと共同で、コーディングエージェントがユーザーの設計意図に厳密に従うことを形式検証によって保証する研究プロトタイプ「PDD Kit」を発表した。本ツールは証明駆動開発（PDD: Proof-Driven Development）パラダイムを導入し、自然言語による要件をRust向け証明言語Verusの形式仕様へと変換する。エージェントがコードと数学的証明を生成し、VerusとZ3ソルバーを通じてあらゆる入力に対する決定論的な機械検証を実行する。
推薦理由
コーディングエージェントが生成する大量のコードを1行ずつレビューすることが困難という課題に対し、本ツールはレビューの重点を自然言語の意図と形式仕様へ移行させ、生成コードのドリフト（意図からの乖離）を解決するための実用的なエンジニアリングパラダイムを提供する。
出典：Microsoft Research · microsoft.com