微軟研究院的 PDD Kit 正式驗證代理撰寫的全端網頁應用程式

微軟研究院推出 PDD Kit，這是一個研究原型，能將開發者的自然語言意圖轉換為 Verus 形式規格，證明編碼代理的 Rust 程式碼對所有輸入皆符合該規格，並在證明無法觸及之處退回測試。在 GitHub Next 的 Chopin 內部示範中，團隊使用 PDD Kit 驗證 Pet Store 的登入邏輯，這是一個約 5,000 行的 Rust 全端應用程式，開發者審查的是意圖產物，而非逐行檢視生成的程式碼。PDD Kit 目前僅驗證 Rust，其保證建立在六個經開發者核准的可信片段上，包括 bcrypt 密碼檢查與兩次資料庫查詢。