智能合约形式化验证工具真能解决问题么？

在智能合约的形式化验证过程中，需要专业的编程人员对不同模板的智能合约进行特征分析、模型建立和模型验证。现在市场上出现了一些一键式的智能合约形式化验证工具，据说可以最大程度的减少验证程序、发现bug，提高工作效率。这种一键式的智能合约形式化验证工具真的有效么？为了求真笔者做了一个测试。

本次笔者测试选择的是成都链安研发的离线版免费验证工具Beosin-VaaS。我们基于VSCode的插件市场安装一个sodility开发插件（具有语法检测，高量和语法联想，方便合约开发。），安装完成后，在插件市场安装成都链安的免费检测工具Beosin-VaaS。
合约代码如下：


我们用成都链安的插件检测一下我们合约中存在的问题
开始检测
我截取部分报错解释说明一下
插件报错会展示行号和那一行的代码以及描述信息，有助于开发人员修改问题

在调用call/send函数后无论执行成功还是失败都不会直接抛异常，如果不对调用返回值进行检查，函数会继续执行，造成安全漏洞。

溢出是典型的合约漏洞，可能导致检查被绕过，合约运行逻辑出错。

Solidity中允许有未使用的变量，它们不会构成直接的安全问题，但会降低代码的可读性并且额外占用存储空间导致部署时的资源消耗增加。

成都链安的检测插件集成了编译器的告警，会提示你一些合约开发中的信息。

在transfer、transferFrom、transferOwnership等敏感函数中，用户操作不可逆，所以建议开发者在这些函数实现中增加目标地址非零检查，避免用户误操作导致用户权限丢失和财产损失。

以上是我们这个合约中部分存在的漏洞报错，有了这个插件的检测，我们就能快速定位解决问题，使我们的合约更加安全。