智慧型合約形式化驗證工具真能解決問題麼？

在智慧型合約的形式化驗證過程中，需要專業的程式設計人員對不同模板的智慧型合約進行特徵分析、模型建立和模型驗證。現在市場上出現了一些一鍵式的智慧型合約形式化驗證工具，據說可以最大程度的減少驗證程式、發現bug，提高工作效率。這種一鍵式的智慧型合約形式化驗證工具真的有效麼？為了求真筆者做了乙個測試。

本次筆者測試選擇的是成都鏈安研發的離線版免費驗證工具beosin-vaas。我們基於vscode的外掛程式市場安裝乙個sodility開發外掛程式（具有語法檢測，高量和語法聯想，方便合約開發。），安裝完成後，在外掛程式市場安裝成都鏈安的免費檢測工具beosin-vaas。

合約**如下：

我們用成都鏈安的外掛程式檢測一下我們合約中存在的問題

我擷取部分報錯解釋說明一下

外掛程式報錯會展示行號和那一行的**以及描述資訊，有助於開發人員修改問題

在呼叫call/send函式後無論執行成功還是失敗都不會直接拋異常，如果不對呼叫返回值進行檢查，函式會繼續執行，造成安全漏洞。

溢位是典型的合約漏洞，可能導致檢查被繞過，合約執行邏輯出錯。

solidity中允許有未使用的變數，它們不會構成直接的安全問題，但會降低**的可讀性並且額外占用儲存空間導致部署時的資源消耗增加。

成都鏈安的檢測外掛程式整合了編譯器的告警，會提示你一些合約開發中的資訊。

在transfer、transferfrom、transferownership等敏感函式中，使用者操作不可逆，所以建議開發者在這些函式實現中增加目標位址非零檢查，避免使用者誤操作導致使用者許可權丟失和財產損失。

以上是我們這個合約中部分存在的漏洞報錯，有了這個外掛程式的檢測，我們就能快速定位解決問題，使我們的合約更加安全。