Concord: Automatically Checking EVM Bytecode Equivalence - DeFi Security Summit 2025
三句話摘要
用形式化等價驗證（Formal Equivalence Checking）搭配 LLM，自動把 Solidity inline assembly 改寫為可讀標準程式碼，並保證語意完全不變。 LLM 改寫程式碼幾乎必然引入微妙錯誤，唯有搭配形式化等價驗證的反饋迴圈，才能讓自動化程式碼轉換真正可信賴。 inline assembly 是靜態分析的剋星：Solidity 允許直接操作 EVM 記憶體（如手動讀寫 free pointer `0x40`），讓 Certora Prover 的記憶體靜態分析無法追蹤，被迫放棄。Concordance 的目標是自動產生語意等價但可分析的標準 Solidity 版本。
重點整理
重點- 1
inline assembly 是靜態分析的剋星：Solidity 允許直接操作 EVM 記憶體（如手動讀寫 free pointer `0x40`），讓 Certora Prover 的記憶體靜態分析無法追蹤，被迫放棄。Concordance 的目標是自動產生語意等價但可分析的標準 Solidity 版本。
- 2
等價的嚴格定義決定驗證品質：等價不只是「return 值相同」，必須涵蓋：相同環境與 calldata 下，兩程式的 revert 狀態、return data、外部呼叫（順序與參數）、event log（相對順序）、以及執行結束後的 storage 狀態全部一致。Gas 消耗、記憶體內容、stack 狀態不列入驗證範圍，因為外部觀察者看不到。
- 3
SMT Solver + Skolemization 解決無限狀態空間比較：比較 storage 或呼叫列表時，不可能逐一比對 2²⁵⁶ 個槽位；改用 skolemization——讓 solver 嘗試「找出任何一個不同的 index」，若找不到則證明兩者完全相等。外部呼叫的 hash 使用 injective uninterpreted function 模擬，避免實作 Keccak256 的複雜性。
- 4
LLM + 形式驗證的反饋迴圈才是關鍵：單靠 LLM 輸出幾乎必然有微妙錯誤（如 ABI decode 對非標準 bool 編碼的 revert 資料不同）。Concordance 的核心價值在於：LLM 生成 → Concord 驗證 → 若不等價則輸出具體反例 → 反例餵回 LLM → 迭代直至通過驗證。
實用技巧與重點
乾貨- 工具名稱：Concordance（外層工具）、Concord（等價驗證核心）、Certora Prover（底層符號推理引擎）
- SMT Solver 組合：Z3、CVC4、CVC5、Bitwuzla，採用 portfolio 策略全部並行，各有不同配置參數
- 反例案例：Solady 的 `safeTransferFrom` inline assembly 改寫後，LLM 版本在返回 buffer 為 31 個 0 + `0x0002`（非合法 bool ABI 編碼）時，原版 revert 帶 "transfer from failed" 訊息，LLM 版 revert 帶空 buffer → 不等價
- 修正方式：將 return data cast 為 `bytes32`，再 cast 為 `uint256`，比較是否嚴格等於 1，而非依賴 ABI decode
- 實際 bug 發現：Vyper 的實驗性 Venom IR pipeline 在開啟最佳化時產生錯誤 bytecode，已被 Concordance 驗證出不等價
- 儲存佈局限制：兩個待比較合約必須使用完全相同的 storage layout，否則驗證必然失敗
- re-entrancy 處理：每次控制流離開合約（call out 或 return）時都必須驗證 storage 狀態一致，不只是函式結束時
- 開源：Concordance 已在 GitHub 開源
結論
結論“LLM 改寫程式碼幾乎必然引入微妙錯誤，唯有搭配形式化等價驗證的反饋迴圈，才能讓自動化程式碼轉換真正可信賴。”
完整解析
詳細在 EVM 智能合約的形式化驗證領域，Certora Prover 需要對 bytecode 進行靜態記憶體分析，才能有效優化最終餵給 SMT solver 的數學公式。然而 Solidity 獨特地允許開發者輕易插入 inline assembly，直接操作 EVM 的原始記憶體與 free pointer。以 Solady 函式庫的 `safeTransferFrom` 為例，它手動讀寫 `0x40`（free pointer 位置），執行完再還原，雖然 gas 效率極佳，卻讓靜態分析工具完全無法推理記憶體使用模式，只能放棄分析。這不只是工具問題——這類程式碼對人類審計者而言也極難驗證正確性。
Concordance 的核心構想是：既然 LLM 擅長程式碼改寫，就讓它把 inline assembly 翻譯成標準 Solidity，再用形式化方法驗證兩個版本行為完全一致。「等價」被嚴格定義為：在相同 calldata 與相同環境（含所有合約的 storage、帳戶餘額、code hash 等）下，兩程式必須有相同的 revert 狀態、相同的 return/revert data、以相同相對順序發出相同的 event log、以相同相對順序發出相同的外部呼叫，且執行結束後 storage 最終狀態相同。Gas 消耗、記憶體內容、stack 狀態因為外部觀察者無法感知，刻意排除在外。
技術實作上，Concord 在 bytecode 層（而非 Solidity 源碼層）插樁，在每次外部呼叫與 log 發出前記錄其 hash。Hash 使用 injective uninterpreted function 模擬，讓 SMT solver 不需要真正計算 Keccak256。比較兩個版本的呼叫列表與 log 列表時，採用 Skolemization 技巧：不嘗試逐一比對，而是讓 solver 嘗試「找出任意一個位置 i 使兩列表在 i 處不同」——若找不到，即證明列表相等。Storage 比較同理。此外，每當控制流離開合約時（無論是外部呼叫出去還是函式返回），都必須驗證 storage 一致，以防 re-entrancy 場景中對方合約呼叫回來讀取不一致的狀態。
實際運作中，LLM 的第一次輸出幾乎不會完全正確。在真實案例中，Claude 改寫 `safeTransferFrom` 的版本在面對非標準 bool ABI 編碼（31 個零 byte 加上 `0x0002`）時，行為與原版不同：原版明確 revert 並帶有錯誤訊息，LLM 版則 revert 帶空 buffer。Concord 自動產生這個具體反例，Concordance 將其餵回 LLM，LLM 據此修正——改用 `bytes32` 強轉加上嚴格比較 `== 1` 的方式處理返回值。這個反饋迴圈持續迭代直到 Concord 確認等價。此外，Concordance 也被用於驗證編譯器最佳化，並在 Vyper 的 Venom IR 實驗性 pipeline 中發現了真實的程式碼生成 bug（上線前已修復）。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
