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

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

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

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