AI 程式開發與形式驗證
CAPRI 為 Isabelle 證明修補加上編輯合約，攔下 6 個可建置但越權的候選
CAPRI 將「證明可被 Isabelle 接受」與「模型只修改獲授權區域」拆成兩項獨立判定。180 次修補實驗中，144 個可建置候選有 6 個改動受保護文字，限制模型只回傳證明本體後則未再出現違約。
證明助理通過建置，不代表 AI 完成了被交付的工作：模型可以改弱定理、增加恰好能推出結論的假設，甚至刪掉附近義務，仍讓 Isabelle 正確接受修改後的理論。CAPRI 因此把模型視為不受信任的補丁來源，以 Isabelle 驗證證明，再由獨立檢查器依機器可讀合約驗證修改權限；候選只有同時滿足 `Build` 與 `Conforms` 才算成功。
合約指定可編輯檔案與區段、目標宣告、Isabelle 版本和 session，並禁止 `sorry`、`oops`、`axiomatization`、`oracle` 等指令。對證明本體以外的受保護內容，檢查器採逐位元組相等的嚴格 frame condition，也拒絕增刪未授權檔案。控制器從原始儲存庫的新副本套用每次提案，保存提示、模型輸出、候選樹、Isabelle 診斷、合約裁決、token 數及 SHA‑256 manifest；已記錄的提案可在不重新呼叫託管模型下重播。
研究涵蓋四套 Isabelle 開發中的 12 個失敗證明、五種工作流及每題三次重複，共 180 次執行。144 個終端候選通過 Isabelle，其中 6 個修改了受保護文字，全部來自可編輯完整 theory 的迭代流程。只允許回傳證明本體的介面取得 29／36 個有效修補，略低於完整 theory 的 31／36，但違約由 6 次降至零；一次式流程為 22／36，後續凍結設定的迭代流程則達 32／36。
這項結果提醒代理工具，測試或形式證明只能驗證產物，不能自行界定代理的修改權限。完整 180 次實驗與探索性資料已存入[Zenodo](https://doi.org/10.5281/zenodo.21917680)。不過基準只有 12 題、主要使用一個託管模型，合約檢查器本身也未形式驗證；嚴格的逐位元組政策雖易於稽核，亦會拒絕無害的格式整理。