Solidity Debugging meets Formal Methods — Raoul Schaffranek | Runtime Verification

智能合約的安全保障長期存在一道隱形門檻：形式化驗證（Formal Verification）能提供數學級別的正確性保證，但高昂的成本與高度專業化的工具，讓這項技術只停留在 Uniswap、Optimism、EigenLayer 等頂尖協議。Runtime Verification 在過去兩年的核心目標，就是打破這道門檻——讓獨立安全研究員和普通開發團隊也能自行運行形式化驗證工具。

第一個切入點是「從調試入手」。開發者天天用調試器，理解調試就能理解符號執行。Runtime Verification 在 Truffle 關閉、VS Code 生態缺少 Solidity 調試器的空窗期，推出了 Symbolic——一款帶符號執行能力的 VS Code 調試器。與傳統調試器只執行一條具體路徑不同，Symbolic 在遇到 `if` 語句時會同時保留兩個執行分支，畫面上出現兩個游標並排前進，並以可視化的控制流圖呈現所有分支。這個設計本質上是「增強版時間旅行調試」——不只能往回走，還能跳到備選的時間線（即合約的備選執行分支），讓審計人員可以直接點擊圖中的節點跳轉到對應程式碼段。目前工具尚缺 Solidity 變數顯示功能（僅能看 EVM 底層的 stack/memory/storage），此功能依賴以太坊基金會正在開發中的新調試格式，預計近期補齊。

第二個切入點是「從測試出發」。講者清楚劃定了三個信心層級：單元測試在固定參數下跑；模糊測試用啟發式採樣（包含常數挖掘）跑數百萬條路徑，結果是「沒找到反例，但不確定是否遺漏」；而符號測試則是對所有可能的輸入狀態執行符號執行，若成功輸出的是機器可驗證的數學證明——「不存在任何參數組合使測試失敗」。這不是量的差異，而是本質上確定性的飛躍。Kontrol 就是實現這個飛躍的工具，它讓開發者直接用 Foundry 語法寫屬性測試，後端以 KEVM（完整 EVM 形式語義）跑符號執行，把「測試套件」直接當作「規格」，省去了自然語言→數學語言的翻譯過程。

在實務流程上，Kontrol 的工作循環是：跑 `kontrol proof` 後，若找到反例就修 bug 再跑；若 prover 卡住，就用 `kontrol show/view` 查看卡住時的 EVM 完整狀態，再手寫 lemma（引理）引導 prover 繼續。這個「引導 prover」的步驟目前仍需懂形式語言，是工具尚未完全降低的門檻，團隊正在研究如何讓 lemma 也能用 Solidity 語法表達。至於效能問題，Kontrol 的計算強度遠高於模糊測試，單次驗證可能需要數小時甚至數天，因此最佳實踐是整合進 CI 流水線，在夜間或每次合併 PR 時自動執行，而非在本機開發週期中阻塞。值得一提的是，Kontrol 是目前極少數能完整推理 Solidity 循環（包含 EVM 位元組碼層的隱性循環）的工具之一，且在公開基準測試 `eth-sc-comp-benchmarks` 中自動求解能力排名同類最佳。