CertiK（shentu）于2018年由哥伦比亚大学计算机系顾荣辉教授与耶鲁计算机系系主任邵中教授共同创立。作为区块链安全领域的先驱，CertiK利用目前最先进的形式化验证技术以及AI审计技术，扫描及监控区块链协议和智能合约的安全性，并不断推出以Skynet（天网）为代表的SaaS产品，为加密世界的企业和用户提供最高等级的安全解决方案。
CertiK（shentu）致力于让人们更加信任区块链，通过利用突破性的技术（包括形式化验证、深度规范技术、自动验证引擎等）来证明区块链项目底层系统的安全性，并开发了一套强大的技术和工具，以确保区块链项目在生命周期的每个阶段（从初始开发到实际应用）都保持安全性和准确性。
此外，CertiK（shentu）还创建了一个审图盾系统，类似于保险，因为虽然CertiK（shentu）提供的安全审计和防御措施可以大大消除代码故障和被恶意攻击的风险，但仍有小概率风险会发生，因此审图盾提供了一个去中心化的社区资金池，当项目方将保险资金投入审图盾池时，将获得CTK的奖励，万一发生风险，CTK也将从相关资金池中支付给遭受损失的项目方，这种保险替代方案提供了更多的保障。
2022年第一季度，CertiK在Web3安全方向的营收有近4倍的同比增长。根据CoinMarketCap数据显示，在使用第三方安全审计的区块链项目中，CertiK的市场占有率超过60%。
本文，我们重点介绍CertiK（shentu）的核心技术“形式化验证”。
什么是形式化验证？
形式化验证的英文名叫Formal Verification，是用数学方法去证明系统无Bug。
首要的一步是用数学语言描述清楚我们要解决的问题。通过对问题建立数学模型，限定系统在不同时刻应该有的状态，以及不应该有的状态。然后用这些数学规则去限定系统的设计以及实现。
传统上在硬件设计领域比较常用。主要原因就是硬件设计周期长，成本高，一旦生产出来就很难改动了。例如一个 CPU 设计如果已经出芯片了，那么出了问题就是大事。比如该部分内容作者以前所在的能源动力领域，很多电厂设备也都要做数学上的论证，不过我们那会儿不用形式化验证这个词，我们叫建模，或者叫软件模拟。如果直接用一台机器去做各种试验，那么成本是很高的，而用数学去构建一台虚拟的机器去验证，既可以运行全部的输入和输出，做到论证充分，同时又没有太高的成本。
总之，形式化验证就是用数学去精确的论证一个系统，可以是硬件系统，但是本文要重点聊的是它在软件开发领域的崛起。
为什么大部分程序员都没听说过？
大部分的程序员可能从来都没用过形式化验证，这是为啥呢？
首先就是因为软件迭代太快了。尤其在互联网领域，创新是不变的主题，对一套系统建立数学模型是有很高的时间成本的，对于要频繁迭代的系统就显得不适合了。
软件很容易升级。跟硬件不一样，软件有了 Bug ，可以连夜修复，很多用户根本不会注意到。万一有用户遇到了 bug ，起码后台数据库的数据一般不会损坏，打个电话，让客服帮忙弄一下，谁家的软件又没 bug 呢？
软件是有测试的。对于没有写过代码的同学可能不太熟悉什么叫做写测试。写测试，也就是去写一些能有验证代码的代码。测试代码中其实往往也会模拟一些输入和输出情况的。形式化验证是超豪华版的测试，用严格的数学论证，保证逻辑没有死角。
总之，软件的形式化验证其实多年来一直也有人搞研究，但是在产业界不是很常见。
为何形式化验证对程序员变得越来越重要？
软件的形式化验证最近的火爆，最直接的触发因素是区块链技术的崛起，但是在整个软件开发行业，也都有这个趋势。
如果事关生死，高成本也值了。比如我们要写控制火车调度的软件，或者写控制医疗设备的嵌入式软件，那么仅仅写几行测试代码，或者交给黑盒测试团队，去覆盖百分之九十九的可能，这是远远不够的。我们需要不计成本的去提高软件的可靠性，这时候形式化验证就很有必要了。对于区块链领域，代码即法律，代码控制着我们的数字身份，控制着我们的智能合约中的资金，这些情况下，如果出了问题，可不是给客服打电话就能解决的，区块链行业中很多人经历过 The DAO 事件，一小段时间内，大家眼睁睁看着黑客不断的把大家智能合约中的钱转走，教训很惨痛。
所以在软件开发领域尤其随着区块链的发展，形式化验证将变得越来越受到重视。