2019 年 7 月 23 日，形式化验证服务商 CertiK 的公链测试网络正式上线。区块链研究平台 Evaluape 表示：CertiK 以智能合约和区块链的安全领域为切入点，为区块链的智能合约和应用提供代码安全服务。形式化验证是一种用数学方式来推演代码逻辑是否符合要求的方式，最早应用于航天、航空、军事等领域的安全方面，技术门槛相对较高。

CertiK 主要通过智能标签技术和分层解构来自动标记验证和分发代码，将这种原本难以实现的证明分解为较小的任务后在打上标签并分发给参与者进行验证，同时允许可扩展其他的验证器接入，验证者提供的单模块的检验结果会被无损整合，使其整合后的验证结果没有偏差，通过这种方式逐渐建立其去中心化的验证网络，有利于智能标签的完善并逐步提高验证效率和安全性。

CertiK 的联合创始人是耶鲁大学计算机系系主任邵中教授与哥伦比亚大学助理教授顾荣辉，二人在耶鲁大学的 FLINT group 已经开发出了反黑客攻击的操作系统 CertiKOS，团队具有良好的学术功底和科研积淀。据项目方消息，CertiK 已经与 Binance、KuCoin、OKEx 和 Huobi 等数字资产交易所，以及 NEO、ICON、Terra 和 QuarkChain 等公链达成合作，截至目前已审计了超过 150 个项目，保护了超过 45 亿美元的资产免受损失，并实现了自主盈利。区块链项目的智能合约漏洞带来的资产损失时有发生，智能合约的安全审计也是区块链项目的刚需。CertiK 的技术模式清晰，团队学术背景扎实，实际落地情况良好，前景值得期待。