争议性在于，用数学推演验证软件程序，在确保不同的网络元件接受指令并以用户的身份模拟执行预定程序的过程中，需要人工输入等技术限制，如何运用各种工具包来整合形式化验证，还存在着诸多制约性的因素。

但 CertiK的出现很好的整合了形式化验证。只要你学过编程，就能很方便地用 CertiK提供的教程说明来测试智能合约的安全问题。

我们来看一看产品：

你要做的，就是打开 CertiK的系统，上传你要检测的智能合约，用 CertiK提供的标记语言，标注好要进行测试的代码部分，按下检测按钮。

检测完毕后， CertiK会给你提供这份智能合约的安全系数，并告诉你哪一块程序存在着错误，并提供详细的解决方案。

当你根据 CertiK的解释进行修改，修改完后再进行测试，直到达到 CertiK 100分的安全评级，你的智能合约就可以避免安全漏洞受到黑客攻击。

是不是很简单！简直是智能合约开发者们的福音，黑客们的噩梦。 CertiK的验证过程体现了化整为零的解题思想，将一个难以证明的大问题拆分为许多容易证明的小问题，然后再将证明过的小问题重新组合回分解之前的较难的大问题，并且保证其中从端到端的正确性（end-to-end guarantees）。 在这个过程中，这些小问题都将发送给整个社区，社区的开发者们可以利用 CertiK提供的方法，也可以运用自己的算法来证明这些问题。一旦某个问题通过多方独立的开发者的验证，那么其便可以用来作为建立其他理论的依据，从而形成互助协作的技术机制和良好的社区氛围。 CertiK是如何让智能合约的安全检测做到如此简单的？

团队

这就不得不提 CertiK背后的团队了：CertiK的联合创始人顾荣辉从清华大学本科毕业，耶鲁大学的博士，现为哥伦比亚大学计算机系助理教授。

CertiK的联合创始人邵中，是普林斯顿大学的博士，耶鲁大学计算机系的主任和 Thomas L. Kempner冠名教授，中科大大师讲席教授，有 20余年的安全领域经验。