5.4 智能合約形式化驗證

軟件的形式化驗證用于確定程序是否按照規范行事。一般使用某種具體的規范語言來描述函數的輸入輸出應該如何相關，并基于此證明程序的輸入輸出的相關性。

智能合約需要形式化驗證。第一，智能合約一旦上鏈不可改變，因此編程漏洞變得不可接受；第二，智能合約是完全公開訪問的，這提供了開放性和透明度，也使其成為黑客攻擊目標。形式化驗證是減少軟件漏洞和攻擊風險的強有效的方法，與傳統方法（測試、同行評審等）相比提供了更高的正確性保證。

目前以太坊智能合約的形式化驗證較難實現，因為以太坊虛擬機EVM不針對第三方提供測試，目前以太坊基金會僅使用機器輔助邏輯推理驗證合約所需的工作量。如果要實現以太坊智能合約的形式化驗證，需要徹底改革以太坊虛擬機EVM使其更容易進行形式化驗證，或者建立全新的語言和虛擬機系統來支持形式化驗證。但無論哪種選擇，都需要制定形式化驗證庫和標準。