PDD Kit 研究預覽：AI 寫的 Rust 如何先核對規格，再用 Verus 證明？
PDD Kit 進入有限研究預覽，將需求、Rust 規格與 Verus 驗證接入代理開發流程。理解前置條件、人工規格審查、無法證明時的測試回退，以及它與既有 Chopin 規劃原型的關係。
PDD Kit 想處理的，是 AI 寫完程式之後，團隊如何確認它真的做到要求。以登入功能為例，幾個密碼測試通過，仍不代表所有錯誤密碼都一定無法登入。
這個落差來自驗證範圍：測試檢查挑出的例子，形式證明則嘗試確認程式在寫明的條件下，是否始終符合指定規格。
GitHub Next 與 Microsoft Research 在 2026 年 10 月 21 日介紹 PDD Kit，進入有限研究預覽，將規劃、Rust 規格與 Verus 驗證接進代理開發流程。
不過證明依據的是人已核准的規格。如果需求沒有寫進去，或輸入被前置條件排除，證明成立也不會替這些部分補上承諾。
我會把它視為值得 Rust 團隊追蹤的驗證研究，尤其適合把心力移到需求與規格審查，而不是把它當成可以放心略過所有審查的工具。
要理解它能多確認哪一層，得先看 PDD Kit 怎麼把一句自然語言需求，變成驗證器真正能檢查的條件。
PDD Kit 如何把人的需求變成可驗證規格？
PDD Kit 先與開發者釐清意圖，再提出形式規格，取得核准後才讓驗證器檢查實作。形式規格就是把「程式應該做到什麼」寫成工具能精確判定的條件。
GitHub Next 的原始公告以登入流程示範，先討論程式和開發者想達成的目標，再提出供 Rust 使用的 Verus 規格，之後才進入驗證。
這和請模型再看一次程式有根本差異。模型可以協助提出規格與證明，驗證工具再檢查實作是否滿足寫下的條件，讓這段關係能接受另一層核對。
因此，規格成為人與工具之間的重要交接。人需要理解條件是否符合需求，工具則負責對這些條件和程式的關係做檢查，兩者處理的是不同問題。
有限研究預覽公開了哪些流程？
官方把規格與證明接入代理開發，但沒有公開一套足以讓任何人立即重現全部流程的完整產品文件。現階段能確認的是官方公告、示範與有限研究預覽範圍。
研究方向與已完成的獨立測試仍有差別，讀者應把有限預覽視為理解方法的起點，取得方式則以研究團隊公布的條件為準。
這並不減少新流程的意義，因為它把討論從「模型看起來有信心」移到「它對哪一份承諾提出證明」。但要看懂承諾的強度，就得先知道驗證器如何工作。
這個流程多出一份明確承諾，讓另一個工具能檢查程式與需求條件的關係。
How do you _guarantee_ your agent's code is correct? You prove it.
— GitHub Next (@GitHubNext) October 21, 2026
Introducing Proof Driven Development Kit (PDD Kit) from @MSFTResearch.
PDD Kit helps turn your plan into a formal spec, then proves the agent's code meets that spec for every input. No vibe verification. PDD Kit… pic.twitter.com/oQqWuL8RFV
Verus 證明的到底是什麼？
Verus 檢查 Rust 程式是否在規格列出的條件下，始終滿足要求，而不是再執行一批測試案例。Rust 是程式語言，Verus 則是替其中一部分程式加入規格與證明的工具。
Verus 官方說明指出，開發者先寫出程式應有的行為，工具再用求解器檢查可執行程式是否在可能的執行中滿足它。求解器負責處理這些邏輯條件，而不是模仿使用者按幾次按鈕。
測試和證明因此有不同工作範圍。測試可以確認這次給定的輸入得到預期輸出，形式驗證則試圖處理規格允許的整類輸入，不必把每一個值都逐一列成測試。
例如，測試可以挑幾個整數，確認函式回傳八倍的結果。但若要保證允許範圍內的每一個輸入都遵守同一關係，就需要把範圍與回傳條件寫清楚，讓驗證器推導。
證明是在執行前檢查
Verus 的做法是靜態檢查，也就是在真正執行程式前，分析程式與規格的關係。它不是每次正式服務收到請求，就再加一套相同檢查一起執行。
官方說明也把目前支援範圍限定為 Rust 的一個子集。因此，不能由「支援 Rust」推論現有 Rust 專案的所有語法、套件與外部互動都可以直接納入同一份證明。
能證明的性質也取決於寫入的規格。若規格只描述數值關係，證明不會因此自動回答網路服務、部署設定或其他未表達的要求。
Verus 的基礎規格文件還把條件分成執行前、執行後，以及程式中途必須成立的敘述。這能讓驗證不只停在「輸出看起來正確」，也檢查中間推導是否維持必要關係。
若程式包含重複執行的迴圈，就可能需要說明每一輪都應保持的規則。例如累計資料時，已處理部分和目前總和之間的關係，不能只靠最後挑幾個輸入測試來解釋。
這些用於驗證的內容會留在原始程式中，供工具檢查，但不會成為最後執行檔的一部分。讀者因此能理解，驗證階段的推導工作，和正式服務每次收到請求所做的運算，是不同時點的成本。
只要證明有條件，規格中的「哪些輸入算數」就會直接影響讀者能相信的範圍。
前置條件為什麼會改變保證範圍？
前置條件規定呼叫端必須先做到什麼，驗證器只對符合這些條件的執行給出對應承諾。這些條件從一開始就是規格的一部分，也決定驗證器處理的輸入範圍。
參與研究的 Alex Lavaee 在 10 月 26 日的說明中，展示一個回傳輸入八倍的函式。輸入是有範圍的整數，因此規格先限制輸入，避免計算結果超出可表示的範圍。
他的例子把允許條件寫成負十六以上、小於十六，再要求回傳值等於輸入乘以八。前半段是呼叫端的責任，後半段才是這個函式承諾交出的結果。
如果實際呼叫送來範圍外的數值，就不能拿原本的證明宣稱那次執行也受到相同保證。這項差別來自規格允許的狀態，增加少數測試例子不會自動擴大原本的證明範圍。
輸入範圍與產品情境要對得上
放回登入情境，團隊就需要確認規格涵蓋的是哪個帳號、哪些輸入，以及什麼狀態下可以發出登入憑證。不能只因為文字提到「正確密碼」，就假設所有帳號狀態也已經寫清楚。
假設一個產品還要求停用帳號不得登入，那就是另一項應被表達的要求。這只是解釋規格範圍的假設例，不是本文發現 PDD Kit 有這個漏洞。
這也說明，嚴格限制輸入可能讓證明比較容易完成，但如果限制排除了產品真正會遇到的情境，證明對實際工作的幫助就會縮小。
當這些條件與真實需求有落差，就應回頭修正人核准的規格，再要求實作與證明對應新的條件。
人審規格，與逐行看程式相比多了什麼責任？
人審規格時，必須確認重要的需求與例外都寫進承諾，而不只是確認文字讀起來合理。代理可以把形式規格整理成容易理解的說明，人仍要判斷這份說明是否涵蓋產品要做的事。
逐行看程式時，審查者可能一邊讀，一邊靠經驗補出沒有寫明的假設。改成先審規格，這些假設就得更明確，否則驗證器不會自動知道人心裡還有另一套要求。
例如，「只允許正確密碼登入」和「正確帳號在允許的狀態下才能取得自己的登入憑證」，對人來說可能很接近，但實際寫成條件時，涵蓋的關係可能不同。
因此，把審查往規格移，不代表人需要理解每一行證明細節，卻代表團隊要能說清楚允許什麼、禁止什麼，以及外部系統提供的資訊被當成什麼條件。
把三種角色分開也有助於理解信任。開發者核准要證明的承諾，代理協助產生實作與驗證材料，驗證器則檢查它們之間是否成立。代理寫出一段證明文字，本身還不是驗證器已接受的結果。
當需求或實作改變，原本的結果也要回到它對應的版本來看。例如新增帳號狀態後，即使舊版登入邏輯曾被證明，仍應先確認新版承諾與程式是否相同，再判斷舊證據還能支持哪一部分。
Chopin 如何保留團隊核准過的決策？
PDD Kit 的公告提到與 GitHub Next 的 Chopin 整合，讓團隊共同規劃。Chopin 是多人即時編輯與討論規劃文件的研究原型，官方專案頁把它的發布時間列在九月。
Chopin 原始專案重視的是決策如何留下，包括誰回答過問題、哪些意見被接受，以及規劃文件如何隨團隊討論更新。這和「已經證明整個系統正確」不是同一件事。
把兩者接在一起的價值，是人核准了什麼較容易被追溯。若需求後來改變，團隊可以先回到那份決策與規格，確認要修改哪一項承諾，再要求新的實作與驗證結果。
延伸閱讀：Claude 寫了九成程式，誰來審？Claude Code 團隊公開分層審查流程
規格能表達的部分可以交給證明工具，碰到無法證明的部分，仍要選擇別的驗證方式。
無法完成形式證明時，PDD Kit 怎麼處理？
官方表示，無法證明的部分會回到測試與電腦操作代理的經驗驗證。電腦操作代理就是能以點擊、輸入等方式操作介面的代理，可以用來檢查實際流程的表現。
這種回退很重要，因為它承認同一個產品的不同部分，可能使用不同強度的證據。有的性質有形式證明，有的只在指定測試中通過，還有的依賴人檢查介面或結果。
如果最後只留下一個「驗證完成」標籤，讀者就看不出哪一項是證明、哪一項是測試。對需要接受審查的團隊而言，證據的種類和涵蓋範圍，應和結論一起留下。
測試仍能檢查規格之外的實際表現
例如，登入邏輯即使有一部分被證明，使用者仍可能需要確認按鈕是否可用、訊息是否清楚，以及與其他服務的接法是否正確。這些觀察不能因為另一層已有證明就自動省略。
反過來，介面操作成功也不能替代底層規格的證明。測試可以發現具體失敗，卻不能單靠成功幾次，就宣稱所有符合條件的輸入都已經被涵蓋。
這和 Anthropic 先前用 Claude 對開源程式庫做形式驗證的研究，也有不同焦點。那篇針對既有程式的特定安全性質，這次則把規格討論接到代理開發前段，不能直接共用成果數字。
所以同一個流程最後可能包含不同強度的證據，團隊仍得把每一項結論與它實際依據分開記錄。
Rust 團隊現在該怎麼看這項研究？
這項研究把檢查重心往需求與規格移，但目前能確認的是有限預覽與官方示範，並非完整產品的獨立驗證。Microsoft Research 的官方確認貼文也把它描述為探索更嚴格的代理開發方法。
因此，現階段值得關注的是規格如何形成、如何被人理解與核准，以及哪些程式可以進入 Verus 的支援範圍。這些問題會直接影響研究是否能用在團隊原有的程式上。
官方安排在十月二十八日至二十九日的 GitHub Universe 展示工作，截至十月二十七日仍是接下來的活動。不能把預告寫成現場已經完成的結果，也不能由預覽推論所有人已能取得相同工具。
對願意把產品要求寫成明確條件的 Rust 團隊，這提供了值得追蹤的方向。但如果需求本身還模糊，省掉逐行看程式不會自動省掉釐清需求的工作，責任只是移到更上游。
延伸閱讀：Claude 形式驗證百餘開源程式庫：239 個入口的證明，保證了哪些安全性？
我會追蹤規格如何被審查、哪些實作能被證明，以及未證明部分怎麼處理，再決定它是否適合團隊的實際程式。
PDD Kit 常見問題 FAQ
PDD Kit 已經正式開放所有人使用嗎？
尚未。原作者稱為有限研究預覽，本文沒有找到可供一般使用者重現全部流程的獨立產品文件或公開安裝來源。
Verus 證明是否代表整個產品沒有漏洞？
不是。證明針對寫明的規格與條件，未納入的需求、範圍外輸入和其他系統部分，不能自動套用相同結論。
測試回退和形式證明是一樣的保證嗎？
不是。測試檢查實際選出的情境，形式證明處理規格允許範圍內的性質，兩種證據需要分開記錄。
