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

在智能合約的形式化驗證過程中，需要專業的編程人員對不同模板的智能合約進行特徵分析、模型建立和模型驗證。現在市場上出現了一些一鍵式的智能合約形式化驗證工具，據說可以最大程度的減少驗證程序、發現bug，提高工作效率。這種一鍵式的智能合約形式化驗證工具真的有效麼？爲了求真筆者做了一個測試。 本次筆者測試選擇的是成都鏈安研發的離線版免費驗證工具Beosin-VaaS。我們基於VSCode的插件市場安裝一個

>>阅读原文<<