PDD Kit 研究預覽：工程師改審規格，讓 Verus 證明 AI 代理寫的 Rust

用 AI 摘要這篇文章：

ChatGPT Claude Perplexity Google Grok

台北時間 2026 年 10 月 21 日深夜至 22 日凌晨，GitHub Next 與 Microsoft Research 的官方帳號加上一位參與計畫的研究員，在同一天先後發出三則訊息，宣布 Proof-Driven Development Kit（PDD Kit，證明驅動開發工具組）進入有限研究預覽。變動本體一句話就能說完：AI 代理寫完 Rust 程式之後，把關方式從「人讀 diff、跑幾個測試」換成「先把需求寫成一份形式規格，再讓驗證器去證明程式對所有符合條件的輸入都成立」。

我的判斷先擺在前面：這套流程真正改變的是審查工作的位置，並沒有把審查工作變不見。人還是要審，只是從逐行讀代理寫的程式，換成核可一份機器可判定的規格；證明蓋不到的地方，官方也明說會退回測試與電腦操作代理。對台灣的 Rust 團隊來說，這是值得追蹤的研究方向，但今天你拿不到它，而且引用它的動機資料時有一個數字陷阱，後面會講清楚。

宣布當天的三則訊息說了什麼

時間軸先對齊。台北時間 10 月 21 日深夜 11 時 58 分，GitHub Next 的官方帳號發布宣傳影片與全文；六分鐘後，參與這項計畫的研究員 Alex Lavaee 接著發出自己的說明；再過幾個小時（台北時間 22 日凌晨），Microsoft Research 官方帳號補上確認貼文。三則訊息指向同一件事：把形式驗證接進代理開發流程。

照官方貼文的描述，流程是這樣走的：代理先跟你討論程式，一邊推斷你的意圖，然後提出一份用 Verus 寫成的形式規格。Verus 是替 Rust 加上規格與證明能力的驗證器。你核可這份規格之後，Verus 自動證明代理寫的程式滿足規格；碰到證不出來的部分，就退回測試與電腦操作代理（CUA）做經驗驗證。官方口號寫得很直白，叫「No vibe verification」，不做憑感覺的驗證；最終目標在貼文裡也寫明了：一座已驗證的軟體工廠，工程師審的是規格，不再是程式碼。

兩個範圍條件值得記住。其一是官方明說今天只支援 Rust，不必學新語言，規格就寫在原來的 Rust 專案裡；其二是它跟 GitHub Next 自家的規劃原型 Chopin 整合，讓規格討論發生在團隊規劃階段。官方也預告會在 10 月 28 日至 29 日於舊金山舉行的 GitHub Universe 現場展示，活動官網顯示實體票已經售完。

誰用得到，誰現在碰不到

適用範圍其實很窄，窄到值得逐項列清楚。

寫 Rust 的團隊是這次唯一被點名的對象。這套流程的前提是你的程式能進入 Verus 的支援範圍，官方參考書對此有但書，下一節會講。

寫 Python、Go 或 JavaScript 的團隊目前完全在範圍外。官方只說了 today works on Rust，沒有給其他語言的時間表，我也不建議用「遲早會支援」來規劃時程。

想現在動手試的人要失望了。我把 githubnext.com 全站的 sitemap 翻過一遍，126 個網址裡沒有任何 PDD Kit 頁面，也沒有看到公開的申請表或安裝文件；官方對一般人的全部訊息就是 limited research preview 這個詞，預覽的名額、申請條件與費用都沒有公布，這幾項在官方進一步說明前都只能當未知。現在能自己動手的是 Verus 本身：開源專案採 MIT 授權，2021 年建立，到我查證的當天仍然有新的提交。至於只用 ChatGPT 寫寫文案的一般使用者，這項宣布對你沒有直接影響。

審查工作被搬到哪裡

先看這套流程想取代的現狀。研究員在貼文裡把業界日常寫得很赤裸：代理產生的程式碼多到沒有人審得完，大家常常把 pull request 的 diff 瀏覽一遍就按下去。同一份焦慮，Google 十月底開源的 Elephant-Goldfish 選擇讓另一個代理在寫碼之前先審設計；PDD Kit 選的是另一條路，把人的核可搬到規格這一層。

搬到規格這一層之後，人審的東西長什麼樣？參與計畫的研究員宣稱，你從此一行程式與一行證明都不用看，只看計畫本身與用自然語言寫下的目標。這是研究方的願景陳述，我要把它跟可驗證的部分分開講：規格的內容是有官方文件可查的。Verus 官方教學把規格定義成四種東西，呼叫前必須成立的前置條件、回傳時必須成立的後置條件、中間的斷言，以及迴圈每一輪都要維持的不變量。這些內容屬於 ghost code，只留在原始碼裡供驗證器檢查，不會被編進最後的執行檔，所以證明是執行前的靜態檢查，執行期沒有額外成本。

Pin

前置條件是整個保證的邊界。驗證器只對符合條件的輸入給出承諾，送進範圍外的值，原本的證明就管不到。官方示範用的例子是登入流程。測試能確認正確密碼登得進去、幾組錯誤密碼被擋下來；證明處理的則是另一個問題：在規格允許的每一種情況下，錯誤密碼都換不到登入憑證。前者是抽樣，後者是對整類輸入的概括保證，這也是「測試通過」與「證明成立」在證據強度上的根本差別。所以審規格時真正要問的是那些容易被略過的問題：哪些帳號狀態被寫進條件了？停用帳號能不能登入有沒有被表達？沒寫進規格的需求，證明不會替你補上。研究員在 10 月 26 日又發了一則用八倍函式講前置條件的說明，把輸入限縮在負十六以上、小於十六的範圍，讓八倍之後的結果仍然放得進 i8，那正是在示範「嚴格限縮輸入讓證明變容易完成」的兩面。

官方也保留了退路：證不出來的部分，退回測試與電腦操作代理。我的解讀是，這條退路讓同一個 pull request 裡從此並存兩種強度不同的證據，一部分是對整類輸入成立的形式證明，另一部分是指定情境下通過的測試。對需要對外稽核的團隊，這兩種證據應該分開標示與留存，如果最後只留一個「驗證完成」的標籤，看的人就分不清哪一段是證明、哪一段只是測過。

研究員引的 42%，在論文裡找不到

宣布貼文裡有一個數字值得停下來查。研究員寫道，近期研究發現最好的 AI 程式碼審查代理第一次嘗試只抓到 42% 的錯誤，並引用一篇微軟研究院與 CMU 合作、2026 年 10 月發表的論文當出處。

我把那篇論文的全文抓下來逐字比對，結果是：全文與表格裡都找不到 42% 這個數字。論文實際的數字長這樣：表現最好的組合是 claude-opus-5 搭配 copilot-cli，第一則評論的抓蟲率是 48.3%（評論軌）與 36.2%（修復軌），到第五則評論分別上升到 79.6% 與 64.2%；論文摘要採用的跨軌平均是 71.9%，五個月前的 opus-4.6 是 47.7%，而且代理仍然漏掉超過兩成人類找到的錯誤。表格裡出現的 42.6 都落在 gpt-5.4 那一組數字，而 gpt-5.4 並不是表現最好的那一個。

Pin

所以方向沒有變，數字要換。審查代理單次評論的抓蟲率確實只有三到五成，「代理寫的程式審不完」這個問題是真的；但要把數字寫進簡報或採購文件的人，應該回到論文的表格，別引用貼文裡的 42%。順帶一提，論文用的基準 CRBugBench 本身規模不小，1,000 個開源任務橫跨 98 個 GitHub 儲存庫，再加上 800 個企業私有儲存庫的任務，這串數字才是這場辯論裡最扎實的證據。

Verus 已經存在四年，但它認得的 Rust 有邊界

PDD Kit 聽起來像新發明，它的引擎卻是個老專案。Verus 在 2021 年 10 月就建立了，自我定位是給低階系統程式碼用的可驗證 Rust，也就是記憶體管理、並行控制這類最容易出錯、也最需要嚴格保證的地帶；MIT 授權、3,475 顆星、到我查證當天仍有提交紀錄。它不是為了代理時代才出現的東西。

但邊界也要說清楚。官方參考書自己寫著，規格語言大致是 Rust 的一個子集，還存在微妙差異，而且專案仍在活躍開發中，部分功能尚未支援。把一個既有 Rust 專案搬進證明流程之前，得先確認用到的語法與相依套件在支援範圍內，不能假設整個生態系的程式碼都能吃。

還有一個脈絡更有意思。Verus 官方書裡已經有一節專門教大家讓 LLM 代理來寫證明：建議在沙箱裡執行、把標準函式庫的內容餵給模型，還警告不給資料的話模型會幻覺出不存在的引理。換句話說，代理寫證明已經是被官方預期的工作形態，當 AI 能夠生產證明，理解該怎麼記功這件事也有人認真討論過。PDD Kit 做的事，是把這條路再往上游推一步，連「把意圖變成規格」都交給代理，人只留下核可權。

Chopin 那一端則把團隊面向補上。這個 2026 年 9 月發布的多人代理規劃原型讓團隊在規劃文件上共同決策，PDD Kit 接上它，規格討論就有了群體審查的入口。兩個都是研究原型，能不能走進日常工作流程，要看接下來的迭代。

Pin

現在可以做什麼

大多數人其實什麼都不用做。這是研究預覽的宣布，還談不上產品上線；等 10 月 28 日至 29 日 GitHub Universe 的現場消息，是最省力的追蹤方式。

寫 Rust 的團隊如果等不及，現在就能動手的只有 Verus 這一半：官方教學與原始碼都是公開的，把既有專案的某個小函式拿來寫規格跑一次證明，就能體會「審規格」與「審程式碼」的手感差異。這個練習的價值在於提前判斷自己的程式碼離證明範圍有多遠。

已經在讓代理寫碼的團隊，不論用什麼語言，可以先在內部討論一個問題：如果審查終究要往規格移，你們的需求文件夠不夠精確到能變成條件？Replit 把代理技能入庫前交給人把關是同一個題目的另一種做法，人的核可放在哪一層，每家都在找答案。值得盯的訊號也有幾個：規格審查的介面實際長什麼樣、既有程式有多少能進證明範圍、退回測試的部分會不會被清楚標示。

回查期限就訂在 GitHub Universe 之後。若官方公開申請管道、完整文件或更多語言的支援，文中關於取得狀態的描述就需要更新。

PDD Kit 常見問題

PDD Kit 現在開放一般人使用了嗎？

沒有。官方定位是有限研究預覽，我在 GitHub Next 全站找不到申請頁面或安裝文件。取得條件以研究團隊之後公布的管道為準。

Verus 證明成立，等於整支程式沒有錯嗎？

不等於。證明只涵蓋規格寫下來的條件：沒被寫進規格的需求、超出前置條件的輸入、規格之外的介面行為，都不在保證範圍內，證明也不會替這些部分補上承諾。查核的動作因此仍然存在，對象從程式碼換成規格條件。

不寫 Rust 的團隊需要關注嗎？

方向值得注意，工具先不用等。「審規格而非逐行審程式碼」這個取捨對任何讓代理寫碼的團隊都適用，但 PDD Kit 目前只支援 Rust，也沒有其他語言的時間表。

回到開頭的判斷。PDD Kit 把審查從程式碼搬到規格，責任沒有變輕，只是換了位置與形狀：以前靠經驗在讀 diff 時補出來的假設，現在要在核可規格那一刻就說清楚。對願意把需求寫成明確條件的團隊，這是個誠實的交易；對需求還說不清楚的團隊，瓶頸會在原地等你。