create-formal-verification-skill | 為高風險性質建立形式驗證
本頁以 pstack-claude 0.9.126 為基準。本次只撰寫教學，不產生或執行形式驗證技能。
定位與適用情境
形式驗證 (formal verification) 用明確性質、假設與範圍檢查程式或模型。此技能先從程式挑選出錯代價高、測試不易涵蓋的承諾，再留下下一位代理能重跑的專案技能。
情境是工作佇列的租約續期與重試可能交錯。要檢查的不變量 (invariant) 是「同一工作同時最多只有一個有效持有者」。輸入是取得租約、續期與釋放程式，以及實際儲存操作的原子性。不能把方便建模的假設誤當成儲存系統真的提供的保證。
準備
- 指定租約相關原始碼、測試、已知故障或風險，以及允許建立驗證檔案的位置。
- 確認工具、版本、安裝權限與可用時間。缺工具時先回報，不假裝已執行。
- 用白話寫出性質與違反後果。另列模型上界、時間抽象、儲存原子性及尚未涵蓋的外部系統。
Claude Code 使用 /pstack:create-formal-verification-skill。Codex 插件選單插入 $pstack:create-formal-verification-skill，skills-only 用 $create-formal-verification-skill。生成位置須採該平台的專案技能目錄。
操作步驟
- 從風險挑目標。 讀取租約相關程式與呼叫端，找出真正承諾及可能交錯的步驟。優先處理重要風險，不為了容易驗證而挑無關小函式。
- 讓問題決定工具。 步驟交錯通常適合模型檢查 (model checking)，原文預設考慮 TLA+。若問題是實際程式的溢位或記憶體安全，則優先找可直接檢查該語言的驗證器。找不到時明說，改用產生式輸入測試真實程式，不把手寫函式模型冒稱程式證明。
- 建立可追溯檢查。 模型的每個動作都要對到可開啟的程式位置，原子步驟要與實作一致。為租約區域建立專案技能，名稱依領域命名，不用
verify或verify-前綴。記錄性質、執行指令、工具版本、涵蓋函式、上界、假設及同步提交 (sync commit)。 - 證明檢查能失敗。 在隔離且可還原的暫存變更中，刻意破壞真實程式所守護的條件，確認生成的驗證流程會捕捉它。還原後重跑，結果應回到原先狀態。若原始程式本來就有反例，應保留並回報，不弱化性質換取通過。
- 以程式語言交接。 說明驗證了什麼、工具選擇理由、反例步驟、重跑方式及未涵蓋部分。若採 TLA+，生成技能應按名稱要求用
statechart解讀結果，不複製可能隨版本改變的內部腳本路徑與參數。
可直接使用的提示詞
用 pstack:create-formal-verification-skill 檢查這個工作佇列的租約流程。
目標是同一工作同時最多只有一個有效持有者。
先讀取得、續期、釋放租約及儲存操作，列出原子性與時間假設。
說明為何選模型檢查或程式層級驗證，再列出要建立的驗證檔案。
若使用有限模型，明列工作數、持有者數與重試上界。
在隔離暫存變更中證明檢查抓得到破壞，之後還原並重跑。
不要修產品程式，不要弱化性質。缺工具或無法安全做破壞測試就回報阻礙。
交付可重跑指令、同步提交、反例及未涵蓋範圍，不提交或推送。預期結果與驗收
- 每個模型動作或驗證條件都能對照實際程式位置。反例應以「持有者甲取得、租約過期、乙取得、甲再寫入」這類程式中的事件解釋，而非只交一段工具輸出。
- 有正常狀態與刻意破壞狀態的執行證據，並確認暫存破壞已還原。從未跑過的技能只能稱為草稿。
- 下一位代理能辨認修改是否碰到涵蓋區域，並知道何時需要重新確認模型與同步提交。
限制與權限
有限模型通過只表示指定假設與上界中的性質成立，不代表整個系統全面正確。抽象模型、產生式測試與無界證明的保證不同，報告不得混稱。
此流程會新增驗證檔案並進行隔離破壞測試。未獲授權不得安裝工具、修改正式資料或修產品。Claude Code 原文採 .claude/skills/<area>/SKILL.md，Codex 不應直接照抄此位置。工具或執行環境欠缺時，應交代未驗證項目。後續同步可用 maintain-formal-verification-skill。