微軟研究院推出 PDD Kit 形式化驗證 AI Agent 撰寫程式碼

針對 AI 編程 Agent 生成龐大程式碼時人工逐行審查難以規模化的問題，微軟研究院提出了證明驅動開發（PDD）流程與配套工具 PDD Kit。該工具在 GitHub Next 的協作規劃環境 Chopin 中運行，引導團隊釐清需求意圖，並轉化為 Rust 形式化驗證語言 Verus 的規格合約，自動生成數學證明以確保程式碼在所有輸入下符合規格。針對驗證器無法涵蓋的第三方函式庫、資料庫查詢與系統時間等邊界，PDD Kit 明確定義可信計算基礎（TCB），要求開發者逐項確認假設並搭配自動化測試驗證。

值得帶走的重點

• PDD Kit 將自然語言意圖轉化為 Verus 形式化規格，驗證 Agent 程式碼在所有輸入下的正確性，非證明範圍則退回測試驗證。
• 工具於 GitHub Next 的 Chopin 協作環境中運作，在實作前透過決策卡釐清自然語言需求的潛在邏輯歧義。
• 微軟研究院在 Rust 全端展示應用中形式化驗證了登入邏輯，開發者不需逐行審查生成碼即證明排除相應規格漏洞。
• 系統明確劃定可信計算基礎（TCB），要求開發者針對第三方雜湊、資料庫查詢與系統時鐘等外部未證假設逐項簽核。