當 coding agent 一次寫幾萬行，逐行 review 已經行唔通
微軟研究團隊 2026 年 11 月 5 日喺 Microsoft Research Blog 發表研究，講點樣用形式化方法（formal methods，一套用數學證明證明程式碼符合規格嘅技術）去驗證 AI coding agent（能編寫程式嘅代理工具）生成嘅程式碼。佢哋嘅結論係：當 agent 一次過輸出幾萬甚至幾十萬行程式碼，靠人逐行閲讀已經行唔通，需要用「數學證明」嚟兜底。
佢哋嘅做法係推出 PDD Kit：將開發者嘅意向轉成 Verus（微軟嘅形式化驗證語言）規格，再對 agent 生成嘅程式碼做數學證明，證明該程式碼對「每一個輸入」都符合規格。證明揾唔到嘅地方，就回退到測試（test）。
「計劃」係合約，但冇人逼 agent 遵守
微軟研究團隊指出，現階段大多數團隊嘅工作流程係：跟 agent 講清楚要做乜 → 反覆修改計劃同測試 → 交俾 agent 實作。呢個「計劃」或者自然語言規格，理上係開發者同 agent 之間嘅合約。
問題係，agent 可以「漂移」（drift）：實作出某啲同預期唔同嘅嘢，然後寫測試去測試「佢自己寫咗乜」，而唔係「你要求佢寫乜」。結果係 CI（continuous integration，持續整合）系統堆滿大量低質測試，覆蓋率表面健康，但「你要嘅」同「實作咗嘅」之間嘅裂口，一直隱藏到 bug report 先至曝光。
資料圖片：Pixabay
測試只能覆蓋程式能處理嘅「一小片」輸入；數學證明則證明對「每一個輸入」都成立。微軟強調兩者互補：證明能達嘅地方用證明，證明達唔到嘅地方用測試。
Pet Store：一個 Rust 網店嘅登入邏輯
研究團隊喺 GitHub Next 嘅 Chopin 平台上試咗呢個方法，對象係 Pet Store，一個用 Rust 寫成嘅網店 frontend。佢哋用 PDD Kit 對登入邏輯做形式化驗證。Verus 證明過程中發現咗已有嘅 bug，並證明「相對於規格，登入邏輯冇 bug」。開發者只審閲咗意向同規格，冇逐行閲讀生成嘅程式碼。
形式化方法：由小眾專家工具變日常工程
過去形式化驗證被認為「太貴」：要專員、唔熟嘅語言、證明文件可以比程式碼大好多倍，開發要經年。微軟指出兩點改變令情況轉變：
- Coding agent 嘅進步令佢哋可以幫手從規格生成形式化證明；
- （原文於此截斷，第二點未完整披露）
PDD Kit 嘅定位係將形式化方法「由小眾專家工作擴展到冇形式化背景嘅工程師，以及日常應用」，例如全棧網店。
資料圖片：Pixabay
模姐驗嚇貨
呢篇研究講緊嘅核心問題係：當 coding agent 嘅輸出規模已超出人類 review 嘅物理極限，我哋點樣確保「寫咗嘅」真係「要嘅」？
PDD Kit 嘅方向有道理——用數學證明兜底，唔係靠人眼。但要留意幾點：呢個研究出自微軟研究團隊，佢哋自家嘅產品（Chopin 亦係 GitHub Next 旗下）；證明範圍受規格限制，規格本身寫錯，證明只係「證明咗同規格一致」，唔代表對。第二點改變佢哋未講完，要等完整版本先至有全圖。
待答問題： 呢個方法真係可以規模化到非微軟產品嗎？Verus 規格嘅撰寫本身又由邊個驗證？
模姐｜深度調教
