理的方法，捕捉、覆蓋合約的所有行為，覆蓋所有可能性，從而保證合約沒有漏洞。第二類是可信：公開透明。合約的創(chuàng)建者不僅要說明白干了什么事，還要向大家證明代碼確實是這么干的。這個也是目前只能用形式化驗證才能做得到。第三類是規(guī)范性問題。前面提到的假充值漏洞，就是因為以太坊的ERC20規(guī)范，寫得非常模糊、不完整。那怎么樣能寫完整呢？這就要求合約的規(guī)范就不能用自然語言，或文字描述，而是應(yīng)該引入形式化規(guī)范，用一種數(shù)學(xué)邏輯語言來嚴格定義。

形式化驗證在工業(yè)界、尤其是安全系統(tǒng)相關(guān)領(lǐng)域，已經(jīng)有了大量應(yīng)用案例，比如航空航天、高鐵、核電等行業(yè)，都有專門的團隊提供形式化驗證服務(wù)，其作用與效果早就得到了安全行業(yè)專家的認可。

目前，形式化驗證包括模型檢驗和演繹推理兩種。安比實驗室（SECBIT）在演繹推理方面積累了十幾年的科研成果和工程經(jīng)驗，技術(shù)在全球比較領(lǐng)先。

相對權(quán)威和安全的公司，比如Zeppelin和以太坊官網(wǎng)都曾經(jīng)公布過有問題的智能合約代碼。如果能有一個更可信，不依賴權(quán)威的智能合約代碼庫，開放給所有人使用，將能很好地解決這個問題。在這方面，安比實驗室（SECBIT）已經(jīng)做了大量工作，并且目前建立全球第一家可信的開源智能合約代碼庫，方便大家免費使用。