智慧合約先寫形式化規格，將人工審查重心轉向行為規則

值得記下的 5 件事

1. [2:00]
   代理加快產出，卻不會自動補齊需求 講者指出，規格未交代的部分，常由開發者自行假設，並可能引入錯誤

   AI 代理同樣會做假設，卻能更快產出大量程式碼與測試，讓人工審查更難負荷。

2. [5:40]
   先寫規格，再讓代理實作與修正 他先自行撰寫形式化規格，再讓代理產生 Solidity 程式碼，由驗證工具尋找違反規則的反例

   這套流程已設為自動化的持續整合工作，遇到反例便讓代理修正；新增功能前，也要先補規格，而非只在專案起點寫一次。

3. [8:40]
   植入錯誤的實驗呈現工具偵測差異 講者刻意植入十一個錯誤，破壞合約應持續維持的性質，也就是「不變量」

   他表示，不變量與模糊測試抓到八個；模糊測試會以大量隨機輸入尋找問題。Certora 則對全部十一個找到反例，但這不代表所有專案都會有相同結果。

4. [13:40]
   訂單簿範例將代幣外部呼叫集中到金庫 他將金庫設為唯一對 ERC20 代幣合約進行外部呼叫的位置，避免規則較複雜的市場模組直接呼叫未知程式碼

   他也試作規格儀表板，並列白話說明與形式化規則，協助安全研究者理解各項要求。

5. [17:20]
   規格是否完整，仍須由人判斷 被問到如何避免遺漏關鍵性質時，他表示仍須審查規則並思考各種情境，不能只因證明通過就認定需求完整

   他也承認，部分性質可能無法證明；規格先行不等於工具已能處理所有驗證難題。