近期，笔者注意到一款智能合约自动形式化验证工具Beosin—VaaS推出了离线免费版。所谓“离线免费版”，相较于之前该公司推出的在线免费版、企业版而言，亮点自然不言而喻。对于开发者来说，离线版的验证工具将提供一个不联网的测试环境，在很大程度上能从根源上将黑客攻击的可能拒之门外。
经笔者测试，虽然这次推出的版本为免费版，但功能毫不逊色，依然能有效检测出智能合约的常规安全漏洞，并精确定位到有风险的代码位置，以及导开发者修改合约代码。对大多数智能合约的安全性而言，需求都已经满足。
尽管笔者认为离线免费版Beosin—VaaS的功能已足够强大，但根据官方发布的消息，对于一些复杂类型的业务合约、以及对安全性要求高的业务合约，还是建议选择企业版Beosin—VaaS或人工审计服务更好。
下面笔者将针对这款离线免费版Beosin—VaaS工具进行简单展述。
1. 什么是形式化验证技术？
其实，形式化验证技术最早是应用于航空、军事等领域的安全关键软件中的技术，本身受众范围没那么广。当成都链安最早尝试将形式化验证技术应用在验证智能合约的安全性上，最后发现审计效果比起传统的验证方式，更具备优势。
形式化验证技术是一种基于数学和逻辑学的方法。具体来讲，在智能合约部署之前，对其代码和文档进行形式化建模，然后通过数学的手段对代码的安全性和功能正确性进行严格的证明，可有效检测出智能合约是否存在安全漏洞和逻辑漏洞。
该方法可有效弥补传统靠人工经验查找代码逻辑漏洞的缺陷，其优势在于，用传统的测试等手段无法穷举所有可能输入，而用数学证明的角度，就能克服这一问题，提供更加完备的安全审计。
2. 什么是Beosin—VaaS工具？
Beosin—VaaS相关工具就是将形式化验证技术应用在对智能合约安全性验证的集大成者。Beosin—VaaS能够面向EVM和WASM智能合约，自动化检测智能合约的10大项32小项常规安全漏洞，为智能合约提供“军事级”的安全保护；并精准定位风险代码位置并给出修改建议；检测准确率>97%，全球最高；从源码到字节码完备的形式化验证；支持多个智能合约编程语言，如Solidity、Go、C++、Python等。
3. 一些Beosin—VaaS的测试实例
笔者选取了655个测试问题进行检测，Beosin—VaaS工具总计检测出635个问题，命中率为96.9%；误报共115个，误报率为15.3%。因此，Beosin—VaaS工具可检测出业务类大多合约案例，具体检测项如下：
通过大体测试，离线免费版自动形式化验证工具Beosin—VaaS在很大程度上都能够满足大多数开发者的验证需要。欢迎大家进行体验。