智慧型合約的形式化驗證
頁面最後更新時間： 2026年2月23日
智能合約 讓建立去中心化、去信任且穩健的應用程式成為可能，不僅帶來新的使用案例，也為使用者釋放價值。 因為智慧型合約掌握了大量的價值，所以對開發者來說，安全是最關鍵的考量。
形式化驗證是提升 智能合約安全 的推薦技術之一。 形式化驗證採用 形式化方法 (opens in a new tab) 來指定、設計和驗證程式，多年來一直用來確保關鍵硬體和軟體系統的正確性。
當在智慧型合約中實作形式化驗證時，可以證明合約的商業邏輯符合預先定義的規範。 相較於其他評估合約程式碼正確性的方法，形式化驗證更能保證智慧型合約功能性上的正確。
什麼是形式化驗證？
形式化驗證指的是一個用形式化規範評估系統正確性的過程。 簡而言之，形式化驗證讓我們可以檢查一個系統的行為是否滿足一些要求（即，它會按我們的想法運作）。
採用形式化模型對系統（此案例中為智慧型合約）的預期行為進行描述，同時藉由規範語言支援形式化屬性的建立。 然後，形式化驗證技術可以驗證一個合約的實作是否符合其規範，並導出合約正確性的數學證明。 當一個合約滿足其規範，則被稱為「功能正確」、「設計正確」，或「建構正確」。
形式化模型是什麼？
在電腦科學中，形式化模型 (opens in a new tab) 是計算過程的數學描述。 程式被抽象成數學函式（方程），模型則描述了給定輸入時如何計算函式的輸出。
形式化模型提供了一個抽象層次，可以在該抽象層次上對程式行為的分析進行評估。 形式化模型的存在，讓人得以建立_形式化規範_，用來描述相關模型所需的屬性。
採用不同的技術來建立智慧型合約模型，以便進行形式化驗證。 例如，有些模型用來推理智慧型合約的高階行為。 這些模型建立技術對智慧型合約套用黑盒檢視，把智慧型合約視為可以接受輸入並按照那些輸入執行計算的系統。
高階模型專注在智慧型合約與外部代理，例如外部帳戶 (EOA)、合約帳戶和區塊鏈環境，之間的關係。 這些模型有助於定義屬性，規定合約該如何回應某些使用者互動的行為。
相反地，其他形式化模型專注於智慧型合約的低階行為。 雖然高階模型有助於推理合約的功能，它們可能無法擷取實作內部運作的細節。 低階模型將白箱觀點應用於程式分析，並依賴智能合約應用程式的較低階表示法 (例如程式追蹤和 控制流程圖 (opens in a new tab))，來推斷與合約執行相關的屬性。
低階模型被認為是理想的，因為它們代表了智能合約在以太坊執行環境 (即 EVM) 中的實際執行。 低階模型建立技術對於在智慧型合約中建立關鍵的安全屬性和偵測潛在漏洞尤其有用。
什麼是形式化規範？
規範不過是特定系統必須滿足的技術要求。 在編程中，規範代表程式執行的總體思路（即程式應該做什麼）。
在智能合約的脈絡中，形式化規範指的是「屬性」—也就是合約必須滿足之條件的形式化描述。 這樣的屬性被描述爲「不變量」，並代表了關於合約執行的邏輯斷言，該斷言在任何情況下都必須為 true，沒有例外。
因此，我們可以將形式化規範想做是用形式化語言編寫的陳述式集合，描述了智慧型合約的預期執行。 規範涵蓋了合約的屬性，並定義了合約在各種情況下應該如何運作。 形式化驗證的目的是確定智慧型合約是否具備這些屬性（不變量）以及在執行過程中不會違反這些屬性。
形式化規範對於開發智慧型合約的安全實作至關重要。 無法實作不變量或在執行期間違反其屬性的合約容易出現漏洞，可能會損害合約功能或導致合約遭到惡意利用。
智能合約的形式化規範類型
形式化規範使程式執行的正確性可以用數學方法進行推理。 與形式化模型一樣，形式化規範可以擷取合約實作的高階屬性或低階行爲。
形式化規範是利用 程式邏輯 (opens in a new tab) 的元素推導而來，程式邏輯可讓人對程式的屬性進行形式化推理。 程式邏輯採用形式化規則來（用數學語言）表達程序的預期行為。 建立形式化規範時，會用到各種程式邏輯，包括 可達性邏輯 (opens in a new tab)、時序邏輯 (opens in a new tab) 及 霍爾邏輯 (opens in a new tab)。
智能合約的形式化規範可大致分為高階或低階規範。 無論規範屬於什麼類別，都必須充分且明確地描述所分析之系統的屬性。
高階規範
顧名思義，高階規範（也被稱爲「模型導向規範」）描述程式的高階行爲。 高階規範將智能合約模型化為 有限狀態機 (opens in a new tab) (FSM)，此狀態機可藉由執行運算在不同狀態之間轉換，並以時序邏輯定義 FSM 模型的形式化屬性。
時序邏輯 (opens in a new tab) 是「針對以時間限定之命題進行推理的規則 (例如：「我『總是』很餓」或「我『最終』會餓」)」。 當應用於形式化驗證時，時間邏輯被用來聲明關於建模為狀態機器的正確系統行為的斷言。 具體來說，時間邏輯描述智慧型合約可以進入的未來狀態，以及它如何在狀態之間轉換。
高階規範通常會捕捉智能合約的兩個關鍵時序屬性：安全和活躍性。 安全屬性代表「任何壞事都不會發生」的想法，且通常表達不變量。 安全屬性可定義一般軟體需求，例如不受 死結 (opens in a new tab) 影響，或表達合約的領域特定屬性 (例如：函數存取控制的不變量、狀態變數的容許值，或代幣傳送的條件)。
以這項涵蓋 ERC-20 代幣合約中 transfer() 或 transferFrom() 使用條件的安全需求為例：「傳送者的餘額絕不低於要求傳送的代幣數量。」。 這種合約不變量的自然語言描述可以轉化為形式化（數學）規範，以進行嚴格的有效性檢查。
活躍性屬性斷言「好事終將發生」，並涉及合約逐步通過不同狀態的能力。 活躍性屬性的一個例子是「流動性」，代表一個合約在收到要求時將其餘額轉帳給使用者的能力。 如果違反此屬性，使用者將無法提領儲存在合約中的資產，就像 Parity 錢包事件 (opens in a new tab) 一樣。
低階規範
高階規範以合約的有限狀態模型作為起點，並定義該模型所需的屬性。 相較之下，低階規範（也稱為「屬性導向規範」）通常將程式（智慧型合約）建模成由數學函式集合組成的系統，並描述這類系統的正確行為。
簡單來說，低階規範會分析_程式追蹤_，並試圖透過這些追蹤來定義智能合約的屬性。 追蹤是指改變智慧型合約狀態的函式執行序列；因此，低階規範幫助指定合約内部執行的要求。
低階形式化規範可以出具為霍爾式屬性或執行路徑中的不變量。
霍爾式屬性
霍爾邏輯 (opens in a new tab) 提供了一套形式化規則，用以推斷包括智能合約在內之程式的正確性。 霍爾式屬性由霍爾三元組 {P}c{Q} 表示，其中 c 是程式，P 和 Q 是 c (即程式) 的狀態述詞，分別被正式描述為_前置條件_和_後置條件_。
前置條件是描述正確執行函式所需條件的述詞；叫用合約的使用者必須滿足該要求。 後置條件是描述函式正確執行時所建立之條件的述詞；使用者在叫用函式後可以預計該條件為 true。 在霍爾邏輯中，_不變量_是執行函數時會保留下來的述詞 (即，它不會改變)。
霍爾式規範可保證_部分正確性_或_完全正確性_。 如果前置條件在函式執行之前為 true，並且如果執行終止，後置條件也爲 true，則合約函式的實作為「部分正確」。 如果前置條件在函式執行之前為 true，執行被保證終止且實際終止時，後置條件為 true，則會獲得完全正確性證明。
獲得完全正確性證明很難，因為一些執行在終止前可能會延遲，或根本不會終止。 也就是説，由於以太坊的燃料機制會防止無限程式迴圈（執行要麼成功終止，要麼因為「燃料耗盡」錯誤而終止），執行是否會終止可以説是一個有爭議的問題。
使用霍爾邏輯建立的智慧型合約規範會具有前置條件、後置條件以及為執行合約中的函式和迴圈而定義的不變量。 前置條件通常包括函式輸入錯誤的可能性，後置條件則描述對此類輸入的預期回應（例如，抛出一個特定例外狀況）。 用這種方式，霍爾式屬性可以很有效地確保合約實作的正確性。
許多形式化驗證框架使用霍爾式規範來證明函式的語義正確性。 也可以在 Solidity 中使用 require 和 assert 陳述式，將霍爾式屬性 (作為斷言) 直接新增至合約程式碼中。
require 陳述式表達了前置條件或不變量，通常用來驗證使用者輸入，而 assert 則捕捉了確保安全所需的後置條件。 舉例來說，可以使用 require 作為呼叫帳戶身分的前置條件檢查，來達成適當的函數存取控制 (安全屬性的一例)。 同樣地，可藉由在函數執行後使用 assert 確認合約狀態，保護合約中狀態變數的容許值 (例如，流通中的代幣總數) 的不變量免遭違反。
追蹤層級屬性
基於追蹤的規範描述了在不同狀態之間轉換合約的操作以及這些操作之間的關係。 如前所述，追蹤是以特定方式改變合約狀態的操作序列。
該方法依賴於智慧型合約模型做為狀態轉換系統，該系統具有一些預定義屬性（由狀態變數描述）以及一組預定義轉換（由合約函式描述）。 此外，控制流程圖 (CFG) (opens in a new tab) 是程式執行流程的圖形化表示，常用來描述合約的操作語義。 在這裡，每個追蹤代表控制流程圖上的一條路徑。
追蹤層級規範主要用來推理智慧型合約中的內部執行模式。 透過建立追蹤層級規範，我們斷言一個智慧型合約的容許執行路徑（即，狀態轉換）。 使用類似於符號執行的技術，我們可以從形式上驗證執行永遠不會追隨未在形式化模型中定義的路徑。
讓我們以一個具有一些公開可存取函數的 DAO 合約為例，來描述追蹤層級的屬性。 在這裡，我們假設去中心化自治組織 (DAO) 合約允許使用者執行以下操作：
-
存入資金
-
存入資金後對提案進行投票
-
在沒有對提案投票的情況下申請退款
追蹤層級屬性的範例可以是_「未存入資金的使用者無法對提案投票」或「未對提案投票的使用者應一律能申請退款」_。 這兩種屬性都斷言了偏好的執行順序 (投票不能在存入資金_之前_發生，申請退款不能在對提案投票_之後_發生)。
智能合約的形式化驗證技術
模型檢查
模型檢查是一種形式化驗證技術，使用演算法對照規範檢查智慧型合約的形式化模型。 在模型檢查中，智慧型合約通常表示爲狀態轉換系統，同時使用時間邏輯來定義許可合約狀態屬性。
模型檢查需要建立系統 (即合約) 的抽象數學表示，並使用以 命題邏輯 (opens in a new tab) 為基礎的公式來表達此系統的屬性。 這樣簡化了模型檢查演算法的工作，也就是說證明數學模型符合給定的邏輯公式。
形式化驗證裡的模型檢查主要用來評價時間屬性，該屬性描述了合約行為與時間的關係。 智能合約的時序屬性包括我們稍早解釋過的_安全性_和_活躍性_。
舉例來說，與存取控制相關的安全屬性 (例如，只有合約擁有者可以呼叫 selfdestruct) 可以用形式化邏輯來編寫。 之後，模型檢查演算法可以驗證合約是否符合此形式化規範。
模型檢查使用狀態空間探索，其中涉及構造智慧型合約的所有可能狀態，並試圖找出導致違反屬性的可達狀態。 然而，這可能會導致無限的狀態數量（稱爲「狀態爆炸問題」），因此，模型檢查器需仰賴抽象技術來實現高效分析智慧型合約。
定理證明
定理證明是以數學方式推論程式（包括智慧型合約）之正確性的方法。 這需要將合約系統的模型和規範轉換成數學公式（邏輯陳述式）。
定理證明的目的是驗證這些陳述式之間的邏輯等價性。 「邏輯等價性」(也稱為「邏輯雙向蘊含」) 是兩個陳述句之間的一種關係，亦即第一個陳述句為 true 若且唯若 第二個陳述句為 true。
關於合約模型及其屬性的陳述式之間的這種必要關係（邏輯等價性），被公式化為可證明的陳述式（又稱定理）。 使用形式化推理系統，自動定理證明器可以驗證定理的有效性。 換言之，自動定理證明器可以結論性地證明智慧型合約模型確切符合其規範。
模型檢查將合約建模為具有有限狀態的轉換系統，而定理證明可以處理無限狀態系統的分析。 不過，這意味著自動定理證明器無法永遠知道邏輯問題是否為「可判定」。
因此，在推導正確性證明時，定理證明器常常需要人類協助給予指導。 定理證明中對人力的使用使其比完全自動化的模型檢查更加昂貴。
符號執行
符號執行是分析智能合約的一種方法，藉由使用_符號值_ (例如：x > 5) 而非_具體值_ (例如：x == 5) 來執行函數。 作爲一種形式化驗證技術，符號執行用於對智慧型合約程式碼中的追蹤層級屬性進行形式化推理。
符號執行將執行追蹤表示為作用於符號輸入值的數學公式，也稱為_路徑述詞_。 SMT 求解器 (opens in a new tab) 會用來檢查路徑述詞是否「可滿足」(即可否找到滿足該公式的值)。 假如某脆弱路徑是可滿足的，SMT 求解器會產生一個具體值來觸發針對該路徑的引導執行。
假設某個智能合約的函數接受 uint 值 (x) 作為輸入，並在 x 大於 5 且小於 10 時還原。 若使用一般的測試程序來尋找會觸發錯誤的 x 值，將需要執行數十個 (或更多) 測試案例，而且不保證能真正找到觸發錯誤的輸入。
反之，符號執行工具會使用符號值 X > 5 ∧ X < 10 來執行函數 (即，x 大於 5 且 x 小於 10)。 相關的路徑述詞 x = X > 5 ∧ X < 10 接著會被交給 SMT 求解器求解。 如果有特定值滿足公式 x = X > 5 ∧ X < 10，SMT 求解器就會計算出該值—例如，求解器可能會產生 7 作為 x 的值。
因爲符號執行仰賴程式的輸入，而探索所有可達狀態的一系列輸入可能是無限的，所以這仍然是一種測試形式。 不過，如範例所示，符號執行在尋找觸發違反屬性的輸入方面比常規測試更有效率。
此外，符號執行與其他隨機產生函式輸入的基於屬性的技術（如模糊測試）相比，產生的誤報更少。 如果錯誤狀態在符號執行期間被觸發，則可以產生觸發該錯誤的具體值並重現該問題。
符號執行也可以提供某程度的數學正確性證明。 仔細思考下面具溢位保護的合約函式範例：
1function safe_add(uint x, uint y) returns(uint z){23 z = x + y;4 require(z>=x);5 require(z>=y);67 return z;8}會造成整數溢位的執行追蹤必須滿足公式：z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y)。這樣的公式不太可能被解出，因此可作為函數 safe_add 絕不會溢位的數學證明。
為什麼要對智慧型合約使用形式化驗證？
對可靠性的需求
形式化驗證被用於評估安全關鍵系統的正確性，這些系統的失敗會產生災難性後果，例如死亡、受傷或金融崩潰。 智能合約是控制鉅額價值的高價值應用程式，設計上的小錯誤就可能導致 使用者無法挽回的損失 (opens in a new tab)。 然而，在合約部署之前進行形式化驗證，則可以增加其在區塊鏈上如期運行的保證。
可靠性是任何智慧型合約都渴求的一種品質，尤其是因爲在以太坊虛擬機 (EVM) 上部署的程式碼通常是不可變的。 合約推出後的升級並不是輕易能夠達成的，形式化驗證成為確保合約可靠性的需求下不可缺少的必需品。 形式化驗證能夠檢測棘手的問題，比如整數下溢和上溢、可重入性和糟糕的燃料最佳化，審核者和測試者可能會漏掉這些問題。
證明功能正確性
程式測試是證明智慧型合約符合某些要求的最常見方法。 這包括用預期合約會處理到的樣本資料來執行合約，並且分析合約的行為。 假如對樣本資料合約傳回預期的結果，則開發者對合約的正確性做了客觀性的證明。
然而，這種方法無法證明樣本資料之外的輸入值也能正確執行。 因此，測試合約可能有助於偵測程式錯誤 (即某些程式碼路徑在執行期間未能傳回預期結果)，但無法斷定沒有程式錯誤。
反之，形式化驗證可以正式證明智能合約在無限的執行範圍內都滿足需求，_完全無須_執行合約。 這需要建立一個形式化規範來準確描述正確的合約行爲，並開發合約系統的形式化（數學）模型。 之後我們可以透過形式化證明程序來檢查合約模型與其規範之間的一致性。
透過形式化驗證，驗證合約商業邏輯是否滿足要求的問題就成爲一個能夠被證明或反駁的數學命題。 透過命題的形式化證明，我們可以在有限的步驟內驗證無限數量的測試用例。 這種方式的形式化驗證在證明合約相較於規範的功能正確性方面具有更好的前景。
理想的驗證目標
驗證目標是指要進行形式化驗證的系統。 形式化驗證最適合用於「嵌入式系統」（作為更大系統一部分的小型、簡單軟體元件）。 也非常適合具有較少規則的專業化領域，因為這樣更容易修改工具來驗證特定領域的屬性。
智慧型合約至少在某種程度上滿足這兩個要求。 例如，以太坊合約的規模較小，這使它們適合進行形式化驗證。 此外，以太坊虛擬機遵循簡單的規則，這使得為以太坊虛擬機中所運行的程式驗證語義屬性變得更加容易。
更快的開發週期
形式化驗證技術，例如模型檢查和符號執行，通常比常規的智慧型合約程式碼分析更有效率（在測試和審核期間的表現）。 這是因為形式化驗證依賴符號值來測試斷言 (「如果使用者嘗試提領 n 以太幣會怎麼樣？」) 而目前常用的測試則使用具體值（「如果使用者嘗試提取 5 個以太幣會怎樣？」）。
符號輸入變數可以涵蓋多個類別的具體值，因此形式化驗證能夠確保在更短時間内覆蓋更多程式碼。 在有效率的使用下，形式化驗證可以加速開發者的開發流程。
此外，形式化驗證透過減少代價高昂的設計錯誤，也改進了去中心化應用程式 (dapps) 的建置過程。 升級合約（如果可能）來修復漏洞，需要大量重寫程式碼基底並投入更多努力在開發上。 形式化驗證可以偵測合約實現中可能會被測試者和審核者漏掉的許多錯誤，並提供充足的機會在合約部署之前修復這些問題。
形式化驗證的缺點
人力成本
形式化驗證，尤其是需要人爲引導證明器來推導出正確性證明的半自動驗證，需要花費大量人力。 而且，建立形式化規範是一項複雜的過程，要求很高的技能水平。
這些因素（人力與技能）使形式化驗證相比評估合約正確性的常規方法（例如測試和審核），要求更高且更加昂貴。 然而，鑑於智慧型合約實作中的錯誤代價，完整驗證審核的成本仍然是可以接受的。
偽陰性
形式化驗證只能檢查智慧型合約的執行是否與形式化規範相符， 因此，確保規範正確描述智慧型合約的預期行為非常重要。
如果規範編寫得很糟糕，就無法透過形式化驗證審核來偵測違反屬性的情況（這會導致執行漏洞）。 這種情況下，開發者可能會錯誤地假設合約沒有漏洞。
效能問題
形式化驗證會遇到一些效能問題。 例如，在模型檢查和符號檢查期間分別遇到狀態和路徑爆炸問題，就可能會影響驗證程序。 另外，形式化驗證經常在其底層使用 SMT 求解器和其他約束求解器，而這些求解器仰賴計算密集型流程。
此外，程式驗證器不一定總能判斷一個屬性 (以邏輯公式描述) 是否能被滿足 (「可判定性問題 (opens in a new tab)」)，因為程式可能永不終止。 因此，即使規範良好，有些合約屬性也可能無法被證明。
用於以太坊智能合約的形式化驗證工具
用於建立形式化規範的規範語言
Act：Act 允許指定儲存更新、前/後置條件和合約不變量。 其工具套件也有證明後端，能夠透過 Coq、SMT 求解器或 hevm 證明許多屬性。
Scribble - Scribble 可將 Scribble 規範語言中的程式碼註解轉換為檢查規範的具體斷言。
Dafny - Dafny 是已可進行驗證的程式語言，依賴高階註解來推斷和證明程式碼的正確性。
用於檢查正確性的程式驗證器
Certora Prover - Certora Prover 是一種自動形式化驗證工具，用於檢查智能合約中程式碼的正確性。 規範是以 CVL (Certora 驗證語言) 編寫，會結合靜態分析與約束求解來偵測屬性違規。
Solidity SMTChecker - Solidity 的 SMTChecker 是一種內建模型檢查器，以 SMT (可滿足性模數理論) 和 Horn 求解為基礎。 它會在編譯期間確認合約的原始碼是否符合規範，並靜態檢查是否有違反安全屬性的情況。
solc-verify - solc-verify 是 Solidity 編譯器的擴充版本，可使用註解和模組化程式驗證，對 Solidity 程式碼執行自動化形式驗證。
KEVM - KEVM 是以 K 框架編寫的以太坊虛擬機 (EVM) 的形式化語義。 KEVM 為可執行檔，能使用可達性邏輯證明某些與屬性相關的斷言。
用於定理證明的邏輯框架
Isabelle - Isabelle/HOL 是一種證明輔助工具，能以形式化語言表達數學公式，並提供用來證明這些公式的工具。 主要應用為數學證明的形式化，特別是形式化驗證，其中包括證明電腦硬體或軟體的正確性，以及證明電腦語言和協定的屬性。
Rocq - Rocq 是一種互動式定理證明器，能讓你用定理來定義程式，並以互動方式產生經機器檢查的正確性證明。
以符號執行為基礎、用以偵測智能合約中易受攻擊模式的工具
Manticore - 一種以符號執行為基礎、用以分析 EVM 位元組碼的工具。
hevm - hevm 是 EVM 位元組碼的符號執行引擎和等效性檢查器。
Mythril - 一種用以偵測以太坊智能合約中漏洞的符號執行工具