新一代公有基础链项目和分布式信任协作平台——本体（Ontology）宣布与美国知名形式化验证公司CertiK展开战略合作，双方将深耕形式化验证领域，增强智能合约和区块链系统的安全性和可靠性。
什么是形式化验证（Formal Verification）？CertiK联合创始人，现任哥伦比亚大学助理教授的顾荣辉表示形式化验证就是用逻辑语言来描述规范，通过严谨的数学推演来检查给定的系统代码是否满足要求。CertiK使用的深度规范技术（DeepSpec）可以将复杂的智能合约转化成模块化的数学模型，通过逻辑推演保证智能合约的安全性。
目前，智能合约具备以下几个问题：由于智能合约的不可逆性，一旦发布在区块链上，合约的源代码将无法被修改；其次，由于大多区块链项目的代码开源，安全漏洞无法隐藏；再者，传统软件安全技术，例如测试与实时监控，都并无法满足区块链极高的安全需求。
本体和CertiK的战略合作将通过深度规范技术及时检测到开源代码的安全漏洞，在智能合约发布前确保安全性与可靠性。CertiK自动化的形式化验证能够避免人为检测的思维局限，最大限度的降低智能合约验证成本，真正实现低成本与高安全性。
CertiK由来自于耶鲁大学、哥伦比亚大学和硅谷的精英团队组成，工程师全部来自Google、Facebook、Freewheel等知名企业。联合创始人邵中是耶鲁大学计算机系系主任，终身冠名教授，顾荣辉是哥伦比亚大学计算机系助理教授。
对于CertiK与本体的合作，顾教授表示：“信任和安全是区块链产业最重要的共识，也是本体和CertiK共同的使命。很荣幸CertiK能与像本体这样优秀且具有前瞻性的项目合作，一起建立安全可信的区块链生态，为区块链世界保驾护航。”
本体创始人李俊认为：“CertiK的愿景是在世界范围内实现透明、公平、安全的区块链生态，这与本体的想法不谋而合。期待未来能与CertiK带来更多关于智能合约形式化验证的实体案例，解决区块链安全痛点，打造高安全性的分布式信任生态。”
