Microsoft Research 的 PDD Kit：AI 寫的程式碼先證明，證明不了再跑測試

AI 幫你寫完全端網頁應用之後，你不用只靠「跑幾個測試看會不會過」來放心，PDD Kit 會先試著用數學證明告訴你，這段程式碼符合你當初講的規格。這是 Microsoft Research 剛推出的工具，目標是解決 AI 程式碼生成裡「計畫」和「實作」脫節的問題。 流程是這樣：開發者把想做的事講出來，PDD Kit 先把意圖轉成 Verus 的形式規格。Verus 是針對 Rust 的驗證工具，規格寫的是「這個函式輸入什麼條件、輸出必須滿足什麼性質」。接著 Agent 生成程式碼，系統去驗證程式碼有沒有符合這份規格。證明得出來的部分就過關，證明不出來的部分，才退回傳統測試。 原理差在覆蓋範圍。測試像出貨前抽檢，你挑幾十個輸入，確認沒壞，沒抽到的就是賭。形式驗證像全檢，證明成立的話，規格範圍內的每一種輸入都涵蓋。這也是為什麼 AI 寫碼特別需要它：Agent 產出程式碼的速度很快，人工 review 追不上，測試又是 Agent 自己寫的話，容易出現「考卷和答案同一個人出」的問題。規格由人的意圖轉出來，驗證的基準就不再依賴 Agent 的自我感覺良好。 目前素材只講了方向，沒有給驗證覆蓋率、成功率或對開發速度的影響，我不會替它補數字。形式驗證本來就很吃規格品質，規格寫歪了，證明得再漂亮也只是證明了一件錯的事。「證明不了就退回測試」這個設計比較務實，等於承認不是每段程式碼都值得或能夠被證明，只把證明用在能證的地方。 我的判斷是，AI 寫碼的瓶頸正從「寫得出來」移到「怎麼知道它對」。接下來比的會是誰的驗證鏈比較完整，而不是誰的 Agent 寫得比較快。