Formal Verification

形式化驗證是一種用數學邏輯證明系統正確性的方法，套用在智能合約上，指的是針對合約程式碼與一份預先定義好的「規格」（specification，通常描述合約在任何情況下都不應該違反的規則，稱為不變量 invariant），用自動化定理證明或模型檢查等數學工具，窮舉檢查所有可能的執行路徑與輸入組合，證明程式碼在數學上確實符合這份規格。這跟傳統的智能合約審計裡常見的測試（testing）與模糊測試（fuzzing）有本質上的不同：測試只能驗證「我們想到並寫下來去跑的那幾種情境」，程式碼裡每多一個條件判斷式，可能執行的路徑數量就會以倍數成長，測試永遠無法窮舉所有路徑；形式化驗證則是透過數學證明的方式，理論上能涵蓋所有可能路徑，而不只是抽樣檢查。

以太坊生態系目前常見的形式化驗證工具包括 Certora Prover（使用專屬的 CVL 規格語言）、Solidity 內建的 SMTChecker，以及各種基於定理證明（theorem proving）或模型檢查（model checking）的學術工具，不同工具在自動化程度、能處理的合約複雜度上各有差異。

形式化驗證之所以被智能合約產業重視，根本原因在於區塊鏈應用一旦部署上線、資產一旦被鎖進合約，程式碼裡的錯誤往往無法像傳統軟體一樣事後補丁修復——很多合約設計上刻意不可竄改，一個藏在極少數執行路徑裡、傳統測試沒有覆蓋到的漏洞，可能造成數千萬甚至數億美元的資產損失，這種「一旦出錯代價極高、且難以事後補救」的特性，正是形式化驗證這類提供數學層級保證的方法特別適合智能合約領域的原因。

以太坊虛擬機（EVM）的執行環境具有確定性（deterministic）與有界（bounded）的特性——同樣的輸入永遠會得到同樣的輸出，且執行過程不涉及傳統軟體常見的無限迴圈或不確定的外部狀態，這個特性也讓形式化的數學方法相對容易套用到智能合約上，相較於通用軟體系統，反而是形式化驗證發揮效果的有利環境。

形式化驗證的實際運作流程，通常從把合約程式碼與 EVM 執行狀態轉譯成一套數學模型開始，這套模型把整個系統表示成一台狀態機（state machine），每一筆交易對應一次狀態轉換；接著開發者或審計人員需要撰寫規格，明確定義這個系統在任何情況下都必須維持哪些不變量（例如「合約裡的代幣總供給量，永遠等於所有帳戶餘額的加總」），這份規格的撰寫品質，直接決定了整套驗證的有效範圍；最後由定理證明器（theorem prover）或模型檢查器（model checker）針對這套數學模型與規格進行推理，如果找到任何一種輸入或交易序列會導致規格被違反，工具會產生一組具體的「反例」（counterexample），標示出確切是哪筆交易組合觸發了違規；如果推理成功，則代表在數學上已經證明，這份規格所描述的性質在所有條件下都成立。

業界目前普遍認為，形式化驗證跟人工審計是互補而非取代的關係：人工審計擅長協助釐清或補齊規格裡遺漏的規則、也擅長判斷業務邏輯本身設計得是否合理，形式化驗證則擅長找出人工審計容易忽略的邊角案例（corner case），尤其在程式碼隨時間持續被修改的專案裡特別有效；但反過來說，定理證明這類方法通常不是完全自動化的，遇到複雜邏輯時往往需要人類專家介入，引導證明器完成推導，這也讓形式化驗證的執行成本與時間投入，普遍比一般測試工具要高上不少。

對一般用戶而言，看到某個專案宣稱自己的合約「經過形式化驗證」，最重要的認知是：這代表合約的核心邏輯，在數學上被證明符合某份特定的規格，但這個保證的有效範圍，完全取決於這份規格本身寫得夠不夠完整——如果開發者在撰寫規格時，遺漏了某條應該存在的規則、或規格本身邏輯有誤，形式化驗證工具根本不會去檢查這條沒被寫進規格的規則，這代表一份合約完全可能在數學上被證明「符合規格」，同時卻仍然存在一個嚴重的漏洞，只是這個漏洞剛好落在規格沒有涵蓋的範圍之外。

Bybit 事件正是這個原則最鮮明的實例：Bybit 使用的 Safe 多簽合約，核心邏輯確實經過業界公認嚴謹的形式化驗證，多年來未曾在協議層級被攻破，但攻擊者完全繞過了合約邏輯本身，鎖定的是簽名者用來「看懂」交易內容的介面層——這一層從未在任何形式化驗證的規格範圍之內，因為形式化驗證從來就不是為了證明「顯示給使用者看的畫面是真的」而存在的。因此看到「經過形式化驗證」這幾個字，應該把它理解成「合約邏輯本身經過嚴謹的數學檢驗」，而不是「這個專案完全沒有安全風險」——這是兩件事，前者是後者的必要條件之一，不是充分條件。