你審規格，機器審程式碼

GitHub Next 和微軟研究院在 10 月 21 日發布了 Proof-Driven Development Kit。它目前是研究預覽版，只支援 Rust，而且它提出的論點，是很多在跑編碼 agent 的團隊一直避而不談的：如果你已經沒辦法逐行讀 diff，就別再假裝可以，換個東西來審。

那個「別的東西」是規格。在 PDD Kit 的流程裡，由人核准 spec，再由機器針對每一種可能的輸入，檢查實作有沒有滿足它。

五個步驟，以及人坐在哪一環

整個循環是這樣跑的。團隊先在 Chopin 裡規劃功能——Chopin 是 GitHub Next 的多人在線 agent 規劃工具。接著 PDD Kit 會討論程式碼、推斷意圖，並提出一份用 Verus 寫的形式化規格；Verus 是既有的、開源的 Rust 證明語言。人核准的是 spec，不是程式碼。然後 Verus 證明 agent 產生的程式碼對任意輸入都滿足這份 spec。在無法給出完整證明的地方，PDD Kit 會退回測試和 computer-use agent 做經驗性檢查，最後產出的是一個已驗證的 pull request。

這個反轉就是全部重點。你審需求，驗證器審實作。在 Verus 裡，spec 用前置條件和後置條件標註函式，驗證器必須把這些條件清掉；而它的保證在某個具體意義上強過一套全綠的測試：測試是抽樣輸入，證明是對所有輸入做量化。

GitHub 自己的說法是，Chopin 加上 PDD Kit，能讓團隊把 AI 產生的程式碼直接送上生產環境而不逐行審閱，保證強度還高於單純的程式碼審查加測試。這是廠商在描述自家的研究預覽版，不是經過稽核的結論。別把它抓得太緊。

{{INLINE1}}

成本只是換了位置，並沒有消失

很容易把它讀成「審查負擔解決了」。並沒有。它被挪到流程的前端，而且變難了，難的程度很容易被低估。

寫一份精確到可以證明的 spec，和審一段 diff，是兩種不同的技能。含糊的需求會產出無法證明的 spec，驗證器會用失敗告訴你這件事，所以導入的頭幾週看起來就像「這工具不能用」。真正發生的是：你需求裡的模糊之處被提早攤出來了，而且是被一個不會用看似合理的函式糊弄過去的東西攤出來的。

對那些一直在寫沒人看的設計文件的團隊來說，這是實實在在的變化。設計文件變成承重結構，因為它是那個會被檢查的產物。

證明止步的地方

有三條限制，比功能清單更重要。

只支援 Rust。Verus 檢查的是 Rust，GitHub Next 說 PDD Kit 目前只在 Rust 上運作，不引入新語言，也不改變程式碼是怎麼產出的。如果你的 agent 寫的是 TypeScript 或 Python，現在沒什麼可裝的。考慮到大量生產程式碼並不是 Rust，這是一句輕描淡寫的話包著一條很大的限制。

只涵蓋 spec 能表達的東西。形式化證明能涵蓋你可以精確陳述的性質：輸入輸出契約、不變式、狀態機轉移。它涵蓋不了 UI 行為、絕大多數 I/O 密集的邏輯，以及任何「正確」是一種判斷而不是一條性質的東西。這些全都落到測試加人工審查的備援路徑上——而那正是今天負擔所在的地方。

研究預覽版，而且有一段很具體的歷史。Chopin 在 GitHub Next 的專案頁上被列為研究原型，日期是 2026 年 9 月。GitHub Next 以前也發布過原型——Repo Mind、Project Copernicus、SpecLang 都在其中——它們從未走到正式可用。第一次針對真實程式碼的公開演示安排在 GitHub Universe，10 月 28–29 日。

備援路徑才是誠實所在

最能說明問題的設計決策，根本不在證明器上。而是它為無法證明的程式碼明確留了第二條路，通向測試和 computer-use agent 的經驗性檢查。

這是大多數驗證工具都拒絕做出的承認。它在架構裡明說：有些程式碼可證明，有些不可證明，假裝不是這樣，比交付兩條流程更糟。用這套東西的團隊最後會給每個模組貼一個標籤——已證明、已測試、已審查——這比任何覆蓋率報告都更誠實地盤點了你的信心。

問題在於，備援路徑也正是 agent 替自己打分數的地方。一個 computer-use agent 點著 UI 檢查改動有沒有生效，它仍然是 agent，仍然在抽樣，仍然可能得出「這個壞掉的流程看起來沒問題」的結論。證明路徑給出的是證明，備援路徑給出的是「一個跑得過的 demo」。

底下那層研究，才是讓人放心的部分

PDD Kit 不是從零打造的驗證器。Verus 是獨立的、成熟的。微軟研究院的 verus-proof-synthesis 儲存庫放著地基：兩個 LLM 驅動的系統 AutoVerus 和 VeruSAGE，負責產生和修復 Verus 證明，分別在 150 個和 849 個驗證任務上做過基準測試。

PDD Kit 看起來新增的是打包。這是這條證明合成研究線第一次被折進一個從規劃到 PR 的產品流程，而不是一次基準測試練習。這個說法比「AI 能證明自己的程式碼」要小，但也更可信。

另外注意，消息來源連名字都沒統一。同一週的報導裡，Proof-Driven Development Kit 和 Property-Driven Development Kit 都會出現，而且都歸到同一個發布上。挑一個用就好；反正做品牌的是那個縮寫。

今天就能做的事

能留下來的結論不是「等 GA」。而是：一個 agent 密集的程式碼庫現在會分成可證明和不可證明兩塊地盤，而你的設定應該已經知道哪塊是哪塊。

解析器、狀態機、資料結構不變式、帶邊界的算術、並行原語——這些是可證明的地盤，Verus 開源、現在就能用，有沒有 PDD Kit 都行。前端的大部分工作、大部分膠水程式碼，以及任何正確性取決於「使用者到底想做什麼」的東西，都不在。

由此有兩個實際動作。第一，在儲存庫裡給可證明的模組打標籤，並讓 agent 專門針對這些模組用 Verus，早於任何廠商交付流程。第二，別再讓 agent 順手寫那些驗證自己工作的測試；這種安排一直是利益衝突，也正是「全綠」比以前更不值錢的原因。

那個讓人不舒服的問題

如果 spec 可以由人核准、證明可以由機器清掉，那審查者到底是幹嘛的？不是讀程式碼，大概也不是抓 agent 在第 412 行引入的 bug。

審查者的工作變成了它本來就該是的那件事：決定這個系統該做什麼，並且拒絕接受一份沒把這件事說清楚的規格。這比在 diff 上按下通過要難。這也是整件工作裡唯一一件驗證器替你做不了的事。