maintain-formal-verification-skill | 讓形式驗證重新對齊程式
本頁以 pstack-claude 0.9.126 為基準。本次文件寫作不會執行驗證器或修改模型。
定位與適用情境
模型通過卻描述舊程式，比明確失敗更容易誤導。此技能從同步提交 (sync commit) 追查涵蓋程式的變更，讓形式驗證 (formal verification) 重新對齊實作，再判斷失敗來自驗證漂移還是真實缺陷。
情境是租約系統把原本一次完成的「檢查持有者並寫入」拆成兩次操作。舊 TLA+ 模型仍把它視為原子動作，因此持續通過。輸入是既有形式驗證技能、模型、執行指令、同步提交及目前程式，不是一般啟動應用程式的 verify 技能。
準備
- 找出真正執行模型檢查器、證明器或程式驗證器的專案技能。沒有就停止，改由
create-formal-verification-skill建立。 - 收集每項檢查的性質、涵蓋檔案與函式、假設、上界、指令及工具版本。
- 若沒有同步提交，原文允許以最後修改驗證檔案的提交為起點，但必須在報告明說此替代依據。
Claude Code 使用 /pstack:maintain-formal-verification-skill。Codex 插件選單插入 $pstack:maintain-formal-verification-skill，skills-only 使用 $maintain-formal-verification-skill。專案技能位置依平台調整，不直接假定為 .claude/skills/。
操作步驟
- 先跑舊檢查。 不改檔先記錄每項原始結果。此時的 pass 只表示舊描述成立，尚不能判斷目前程式是否符合性質。
- 讀取所有相關變更。 比對同步提交到目前提交的涵蓋檔案及提交說明。追查函式搬移、拆分與新增寫入同一狀態的路徑。將變更分為無影響、驗證不再描述程式、承諾刻意改變，或承諾可能被破壞。
- 依程式更新驗證。 在租約案例中，把模型原子動作拆成與實作一致的兩步。只有文件、測試或變更紀錄明確支持承諾改變，才修改性質，並記錄新舊文字及證據。不能按照怎麼做才會通過來調模型。
- 重跑並判讀。 通過時，用隔離暫存變更破壞受保護條件，證明新版檢查仍會失敗，再還原。失敗時逐步將反例對照真實程式。走不通的步驟先視為模型問題，所有步驟都可發生才回報產品缺陷，並追查引入提交。
- 更新技能及交接。 更新涵蓋範圍、指令、上界、假設與已確認的同步提交，再按技能跑一遍。受阻的檢查不得前移同步提交。驗證更新與產品修正分開交付。
可直接使用的提示詞
用 pstack:maintain-formal-verification-skill 查核現有租約驗證是否仍描述目前程式。
先跑未修改的檢查，再從各自同步提交讀取所有涵蓋程式變更。
特別核對持有者檢查與寫入是否仍是同一原子操作。
只改模型、驗證腳本、性質檔與該形式驗證技能，不改產品程式。
性質若要改，列出舊承諾、新承諾及刻意改變的來源證據。
通過後做可還原的破壞檢查；失敗則逐步對照真實程式並追查引入提交。
每項回報 in sync、updated、bug 或 blocked，說明上界及未涵蓋部分。
受阻時不要前移同步提交。不提交、不推送或開 PR。預期結果與驗收
每項檢查都有獨立結果，不能以單一綠燈概括所有檢查。
in sync表示相關變更未影響描述，且檢查通過。updated表示驗證已對齊目前程式，且檢查通過。bug表示描述已對齊，但真實程式會違反性質。更新模型後才暴露缺陷時，可同時標示 updated 與 bug，不能隱藏舊 pass 建立在過期描述上的事實。blocked表示無法完成對齊或執行，應列出阻礙與未前移的同步提交。
報告還應包含讀過的提交、每項修改理由、重跑結果、破壞檢查、反例造成的傷害及未涵蓋的新程式。
限制與權限
通過仍受模型、工具、上界與假設限制，不保證系統全面正確。若必須縮小上界，報告要明說，不能把較弱的覆蓋冒稱等價驗證。
預設只修改驗證，不修產品。不因模型指出缺陷就自動獲准提交產品測試或修正。破壞測試只能在事先界定、可還原的隔離範圍執行。同步提交是查核紀錄，不是用來讓未完成工作看起來已覆蓋的版本標籤。