形式化驗證

形式化驗證以數學方式證明一個合約對每一種可能的輸入與執行路徑都滿足某個指定的性質，而非只檢查少數幾個精心挑選的例子、再寄望其餘也乖乖照辦。測試只能在你試過的案例上顯示漏洞的存在；形式化驗證則力求就一份精確規格而言顯示漏洞的不存在。你寫下什麼必須永遠為真，工具便要麼產出一份它成立的證明、要麼給出一個具體的反例，也就是一串打破它的呼叫序列。

就機制而言，這個性質被編碼成一份形式規格，常是一條不變量，例如代幣總供給永遠等於所有餘額之和，或是一個把函式輸入與輸出相關聯的後置條件。驗證引擎接著以符號方式、而非具體方式探索程式行為：它用 SMT 求解器、定理證明器或符號執行，對合約在符號值上進行推理，一次涵蓋所有路徑。此領域的工具包括帶有 CVL 規格語言的 Certora Prover、Solidity 內建的 SMTChecker、Halmos、K 框架，以及像 Manticore 這類符號執行引擎。

形式化驗證是現有最強的保證，但其威力受限於你所指定的內容。它只證明你實際寫下的性質，因此對一份不完整或錯誤規格的正確證明，會給出虛假的信心。困難而昂貴的工作在於選對不變量、並忠實地建模環境；除此之外，求解器在複雜程式碼上可能逾時，無上限的迴圈也難以完全證明。它最適合用來鎖死高價值合約最關鍵的不變量，並與審計和模糊測試並用，而非取而代之。