2017年耶鲁大学的邵中教授及哥伦比亚大学的顾荣辉教授创办了CertiK。迄今为止，CertiK团队在近两年的发展中异军突起，也即将迎来两周年纪念日。

2015年，团队的联合创始人邵中博士和顾荣辉博士即开始筹备CertiK项目。彼时，由于软件的代码监测方式具有相当大的局限性，两位教授决定精研形式化验证技术，并发现了这种可从数学层面保证软件安全性的技术对行业所能带来的巨大益处。

形式化验证技术在当时便应用于了美国航天局的火星探测器和航空航天设备等与关键任务硬件有关的程序上，但是并没有成为主流应用。

随着邵教授和顾教授的不断深入研究，他们发现，在应用层次，主要的安全威胁来自于不规范的编码，而非实际运算过程。他们开创了Deep Specifications（一种深层规范）方法，将一个非常复杂的事项分解成许多更小、更容易解决或证明的小模块。他们发现，一旦可以证明每一个子模块，就可以把这些对小模块的证明集合起来，再提交端到端的全面审查。

DeepSpec是耶鲁大学、哥伦比亚大学、麻省理工学院、普林斯顿大学和宾夕法尼亚大学共同的研究成果，同时它也获得了美国国家科学基金会(National Science Foundation)的资助。

2016年，邵教授和顾教授用DeepSpec创建了CertiKOS：世界上第一个，也是唯一一个经过完全验证的程序管理/操作系统内核（团队已在维基百科上添加形式化验证词条）。CertiKOS作为军用级别的飞地，可以安全高效地运行软件程序。

DeepSpec开发出的认证技术取得了成功后，邵教授和顾教授认为，同样的技术也可以广泛应用在区块链和智能合约领域。DeepSpec技术可以将智能合约中的复杂证明任务分解为更小的任务，同时在适当的抽象级别验证每个任务。与此同时，通过创建DeepSEA函数式编程语言，CertiK进一步提高了区块链的安全性。DeepSEA允许源代码（如智能合约）在Coq交互式证明助手中运行，生成自动数学证明。

CertiK正式成立于2017年12月21日，拥有世界级的安全团队。运营至今，CertiK已进行了200多次审计，保护了价值超过62.3亿美元的资产。不仅如此，团队也对CertiKOS和DeepSEA继续进行了研究和开发，并公开发布了CertiK链的测试网。

2019年，为了更好的应用落地和满足需求，区块链技术在不断地发展中。作为区块链领域里的新兴技术，形式化验证可以为任何人服务。无论你是否是区块链生态系统的积极参与者，都可以完全放心地使用该生态系统——因为CertiK会帮你消除哪怕只有0.00000001%被攻击的可能。

年度奖项

CertiK荣登榜单，斩获“OKEx 最佳安全审计合作伙伴奖

此次CertiK团队迎来两周年生日，我们非常感谢每一位支持我们保护区块链安全性的用户以及一直以来对我们的支持。

在未来，CertiK将继续为区块链的安全保驾护航，致力于构建健康的区块链生态。

CertiK全体人员致上

请点击“阅读原文”访问CertiK官方网站