Microsoft Research、PDD Kitを実証

Microsoft Researchは、開発者の意図を形式仕様に変換し、あらゆる入力についてコードが仕様を満たすか証明するツールキット「PDD Kit」を発表しました。証明で確認できない要件にはテストを使います。形式手法の専門知識がないエンジニアにも使いやすくすることを目指しています。Microsoftは、Rust製のフルスタックWebアプリ「Pet Store」のログイン処理で実演し、Verusによる証明で指定された性質を確認するとともに、既存のバグを見つけました。開発者は生成コードを一行ずつ読むことなく、意図を確認しました。

Microsoftによると、コーディングエージェントは数万行から数十万行に及ぶ機能を作れるようになり、一行ずつ確認する方法では対応が難しくなっています。計画書には開発者の希望を記録できますが、エージェントが計画から外れたり、自らの実装に合格するテストを書いたりする可能性があります。テストは一部の入力しか扱わないため、当初の依頼と矛盾するケースを見逃すことがあります。PDD Kitは指定された性質をすべての入力について証明で確認し、証明の対象外の動作はテストで確認します。

PDD Kitは、GitHub Nextの共同計画環境「Chopin」内で動作します。開発者に意図について質問し、関連コードを説明したうえで、合意した要件を「意図アーティファクト」に記録します。これは要件を形式仕様とテストにつなぎます。形式化できる要件にはVerusの証明を生成し、それ以外にはテストを用意します。Pet Storeの実演では、開発者は正しいパスワードが必要なこと、管理者アカウントだけが管理者用トークンを受け取ることを求めました。PDD Kitが「正しいパスワードなら常にトークンを発行する必要があるか」と尋ね、開発者は要件が両方向に成り立つことを確認しました。また、リクエストからトークンまたはHTTPエラーにつながるコードも証明に含めるよう選びました。

Pet Storeは約5,000行のRustで構成されています。バックエンドはAxumとSQLiteを使い、在庫、販促、注文、決済を扱います。Leptos製のストア画面はWebAssemblyにコンパイルされます。Microsoftは機密性の高い部分としてログインに焦点を当て、同じ手順をアプリ全体の機能的正しさの確認にも使えると述べました。ログインの証明は、bcryptによるハッシュ化、データベースへの問い合わせ、トークン署名、現在のデータベースの内容、時計、リクエストの完了可否、利用者向けメッセージ、指定されていない要件までは対象にしません。これらは証明の外側にあり、明示的な前提またはテストに依存します。

PDD Kitは、証明が依存するコードと前提を「信頼計算基盤」として可視化します。開発者が承認した前提は6つで、顧客アカウントと管理者アカウントの検索、パスワード確認、トークン生成、時計の読み取りからちょうど24時間、つまり86,400秒後にトークンを失効させる関数、データベースのエラー処理、ログインハンドラーの骨組みです。PDD Kitは、信頼する処理を契約を仮定した小さな関数で囲み、仮定した各条項をテストする計画を立てます。計画では各確認項目を実行前は予定として示し、実行後にコマンドの結果を記録します。

Microsoft Researchは、開発者の意図を形式仕様に変換し、あらゆる入力についてコードが仕様を満たすか証明するツールキット「PDD Kit」を発表しました。証明で確認できない要件にはテストを使います。形式手法の専門知識がないエンジニアにも使いやすくすることを目指しています。Microsoftは、Rust製のフルスタックWebアプリ「Pet Store」のログイン処理で実演し、Verusによる証明で指定された性質を確認するとともに、既存のバグを見つけました。開発者は生成コードを一行ずつ読むことなく、意図を確認しました。

Microsoftによると、コーディングエージェントは数万行から数十万行に及ぶ機能を作れるようになり、一行ずつ確認する方法では対応が難しくなっています。計画書には開発者の希望を記録できますが、エージェントが計画から外れたり、自らの実装に合格するテストを書いたりする可能性があります。テストは一部の入力しか扱わないため、当初の依頼と矛盾するケースを見逃すことがあります。PDD Kitは指定された性質をすべての入力について証明で確認し、証明の対象外の動作はテストで確認します。

PDD Kitは、GitHub Nextの共同計画環境「Chopin」内で動作します。開発者に意図について質問し、関連コードを説明したうえで、合意した要件を「意図アーティファクト」に記録します。これは要件を形式仕様とテストにつなぎます。形式化できる要件にはVerusの証明を生成し、それ以外にはテストを用意します。Pet Storeの実演では、開発者は正しいパスワードが必要なこと、管理者アカウントだけが管理者用トークンを受け取ることを求めました。PDD Kitが「正しいパスワードなら常にトークンを発行する必要があるか」と尋ね、開発者は要件が両方向に成り立つことを確認しました。また、リクエストからトークンまたはHTTPエラーにつながるコードも証明に含めるよう選びました。

Pet Storeは約5,000行のRustで構成されています。バックエンドはAxumとSQLiteを使い、在庫、販促、注文、決済を扱います。Leptos製のストア画面はWebAssemblyにコンパイルされます。Microsoftは機密性の高い部分としてログインに焦点を当て、同じ手順をアプリ全体の機能的正しさの確認にも使えると述べました。ログインの証明は、bcryptによるハッシュ化、データベースへの問い合わせ、トークン署名、現在のデータベースの内容、時計、リクエストの完了可否、利用者向けメッセージ、指定されていない要件までは対象にしません。これらは証明の外側にあり、明示的な前提またはテストに依存します。

PDD Kitは、証明が依存するコードと前提を「信頼計算基盤」として可視化します。開発者が承認した前提は6つで、顧客アカウントと管理者アカウントの検索、パスワード確認、トークン生成、時計の読み取りからちょうど24時間、つまり86,400秒後にトークンを失効させる関数、データベースのエラー処理、ログインハンドラーの骨組みです。PDD Kitは、信頼する処理を契約を仮定した小さな関数で囲み、仮定した各条項をテストする計画を立てます。計画では各確認項目を実行前は予定として示し、実行後にコマンドの結果を記録します。