人が意図を確認し、Verusの仕様へ変換して実装を証明します。Rust製ウェブアプリのログイン処理を例に、証明できる部分とテストで確かめる部分を明示しました。 開発チームでは仕様の不足と信頼する外部部品を先に確認します。証明の対象外まで安全性が保証されたと受け取らないことが焦点です。 大量の生成コードを意図に結び付ける Microsoft Researchは11月5日、PDD Kitを使った開発手順を紹介しました。AIが大量のコードを作る状況で、人の依頼と実装のずれをどう検出するかを扱います。生成した実装に合わせてテストも作ると、試験を通過しても最初の意図を満たさない可能性があります。PDD Kitは、人が自然言語で意図を確認した後、形式化できる部分をVerusの仕様へ変換します。仕様に対して実装を証明し、証明が届かない部分にはテストを使います。GitHub Nextの共同計画環境Chopin内で動く仕組みです。コードを読む量だけを減らすのではなく、何を保証したかを明示する開発を目指しています。 ログインの条件を曖昧なまま実装しない 紹介例は、約5,000行のRustで書かれたPet Storeというウェブアプリです。記事ではログイン処理に焦点を絞っています。正しいパスワードの場合だけトークンを出す、という依頼にも解釈の余地があります。全員を拒否する実装でも、その一方向の条件だけは満たせるためです。そこで正しい入力なら必ず成功する条件も含めるかを、人に確認します。対象となるのは、認証や権限を含む処理をAIで作る開発チームと見られます。仕様の穴を実装後に探すだけでなく、計画時に選択肢として示す点が特徴です。記事の例でログインを検証したことを、アプリ全体の安全性を証明した結果とは扱えません。保証は、合意した仕様と、その仕様が表す範囲に結び付きます。 証明とテストの境界に承認を残す 形式検証は、指定された性質をすべての入力について示します。一方、外部の暗号ライブラリや画面などには、実行して観察する検証を使います。PDD Kitは、証明の前提として信頼するコードの範囲を明示します。利用側では、この境界の妥当性を確認する担当者が必要と見られます。より多くの処理を証明対象にすると、外部との接続部分に置く前提も変わります。証明済みという表示だけで判断せず、前提に含めたデータベースや署名処理を読むことが論点です。導入負担は、仕様を定める時間、証明の保守、実行試験を合わせて測る必要があると考えられます。既存のテストを一律に置き換えるのではなく、重要な処理から保証範囲を増やす方法を原文は提案しています。 仕様の正しさは人が確かめる対象 数学的な証明が成立しても、仕様そのものが依頼を十分に表しているかは別の確認です。原文の流れでは、計画と信頼境界について人の承認を求めています。次の判断点は、自社の要求をどの程度明確な条件へ落とせるかです。拒否すべき入力だけでなく、成功すべき入力も定める必要があると見られます。変更時には、コードだけでなく、仕様と前提がどう変わったかをレビューする体制が重要になると考えられます。仕様を変更した理由も、合意の記録として残すことが考えられます。