在区块链技术领域，智能合约一直在多语言开发环境中发挥着至关重要的作用。如此一来，保证智能合约的安全显得尤为重要。基于这样的背景，本体生态伙伴成都链安（Beosin）推出以太坊后全球第二个高度自动化智能合约形式化验证平台——VaaS-ONT 。

早在去年 7 月，成都链安加入本体“共建者计划”，与本体共同聚焦于区块链智能合约开发 、 安全审计 、 形式化验证 等领域，以提高智能合约和底层链平台的安全性，进一步打造安全、放心、可靠的区块链基础设施。VaaS-ONT 作为成都链安继以太坊后开发的第二个公链形式化验证安全产品，已在本体智能合约集成开发环境 SmartX 中深度集成。

本体智能合约集成开发环境 SmartX

VaaS-ONT 依托成都链安形式化验证技术在民航、军事领域多年的深厚积累，带来 “军事级”形式化验证服务。相较于人工审计智能合约的传统安全防护手段，VaaS-ONT“一键式”形式化验证工具能够精确定位到有风险的代码位置，迅速找出原因，有效验证智能合约或区块链应用的常规安全漏洞、安全属性和功能正确性，从而显著提高安全等级。

开发者可通过进入 VaaS-ONT 产品官方链接全方位体验：

https://smartx.ont.io/

VaaS-ONT 产品页面

关于形式化验证

基本介绍

形式化方法是计算机科学中一种面向软硬件的基于规约、开发以及验证的数学方法。将形式化方法应用于软硬件设计的动机，是为了使其如其他工程规范一样，借助于数学分析的方法加强系统的可靠性和稳固性。

为基于符号执行的模型检测技术形式化验证工具设计原理图

在区块链智能合约领域，形式化验证使用 数学和逻辑语言 精确定义智能合约、智能合约的运行环境以及智能合约的 正确性 和 安全性，并通过数学证明和逻辑推理来证明智能合约的确满足其正确性和安全性定义。与传统测试方法相比，形式化方法通常更加精确，并严格地保证较高的覆盖率。在正常的开发过程中形式化验证方法与其他保证安全的方法有机结合为区块链安全提供保障。

本体形式化验证工具主要验证功能

1、静态检测 ：该部分编译器本身已完成大部分基本检查，可配合编译器做更多检查；
2、动态检测 ：也是形式化验证工具最有价值的部分。细分为：除 0 检测、数组越界检测、断言检测、Require 检测、溢出检测、存储注入攻击检测等。

详见《本体形式化工具检测功能列表》：

操作步骤

1.1 登录 SmartX

使用 Chrome 浏览器访问 https://smartx.ont.io/ ，可以点击下方图标使用第三方 GitHub 账号进行登录；

1.2 创建项目

登录成功后，通过 Create Project 按钮创建项目，目前形式化验证仅支持 Python 版本；

选择项目语言

1.3 编写智能合约

通过为您提供的合约模板快速创建并编辑合约；

1.4 编译智能合约

编写完合约后，选择编译器版本为 version 2.0 （目前形式化验证仅支持 2.0 版本），点击 Compile 进行编译；

1.5 智能合约形式化验证

编译成功后切换到 Verify 页签，点击 Formal verification 进行形式化验证，验证结束后结果将显示在页面右侧。