「Certik」是一家用形式化验证技术保护智能合约和区块链生态的安全的验证平台，致力于应用形式化验证技术，为智能合约和区块链生态提供安全保护。lxK一点就转

lxK一点就转

CertiK的核心产品是CertiKOS防黑客操作系统，采用了形式化的验证 (formal verification)，将智能合约转化为数学模型，通过逻辑上的推理演算来验证模型，从而证明智能合约的安全性。lxK一点就转

这个系统共花费千万美元的科研经费，两位创始人邵中和顾荣辉用6年多研究安全系统，目前CertiKOS不仅在商业市场中通过验证，也被应用到军事防御系统上，并引起了耶鲁大学等美国学术界的关注。lxK一点就转

CertiK的商业模式分两步走：lxK一点就转

1、依靠CertiK自身算力的中心化验证服务。如果客户本身有强大的硬件设备和系统，可向CertiK提交智能合约和需求，CertiK将合约转化为数学模型，进行形式化验证，并生成报告，指明合约中哪一行可能出现漏洞，系统在什么状态或条件下可能被侵入(具体步骤可参考demo演示)。CertiK根据合约的复杂程度收取不同的服务费。lxK一点就转

2、去中心化的安全验证生态系统，借助社区参与者的算力，共同生成报告。前文提到的分层结构理论可将复杂任务拆分成小的模块，CertiK接到客户需求后，将“任务”和技术工具分发给社区，奖励提供算力、帮助检验小型模块的贡献者。交叉验证机制可以确保社区内无人投机取巧、没完成任务还“骗取奖励”。CertiK认为，这种任务分发要比算hash值挖矿更有意义、更低能耗。lxK一点就转

CertiK平台特色：lxK一点就转

1、智能标签——CertiK平台设计了一种新颖的方法来指定DApps /系统使用标签。这些标签具有足够的表现力，可以正式声明期望的属性并且与现有的编程语言兼容(例如，密实度)。通过利用手动建立标签的深度学习技术代码库的培训，CertiK平台打算引入一个框架，命名为智能标签，不仅在语法层面理解分散式程序而且在语义层面上，可以自动向源代码添加适当的标签。lxK一点就转

2、基于层的分解—— CertiK团队是首批实现模块化的团队之一，通过实现一种新的概念进行验证，命名为分层深度规范。这种技术揭示了分层设计模式的见解并使其成为可能将复杂的证明任务分解成更小的模块，并在他们的每个人身上验证他们适当的抽象层次。lxK一点就转

3、可插入的验证引擎——这些分解的证明义务更容易解决，甚至可以通过一些自动验证器来解决。为了实现可扩展性，CertiK平台旨在提供开放协议，这样更高级的求解算法可以自由地插入到这个系统中。lxK一点就转

4、机器可检验的证明对象—— CertiK平台构建机械化证明对象(或反例)，以便这些证明可以被任何人快速检查使用自己的机器。这些证明对象可以被看作是“证书”到已验证的程序。lxK一点就转

5、认证的DApp库——为了提高整个区块链社区代码的质量和可靠性，CertiK平台提供了一系列认证库和插件集成开发环境(IDE)以构建更多值得信赖的DApps。使用这些工具将花费少量的CTK虚拟加密“燃料”，但会在开发期间提供更多的保证。lxK一点就转

6、定制认证服务——对于高可靠性的DApps /系统(例如数字钱包)CertiK平台有意提供定制认证服务。在这种情况下，验证专家将帮助指定/验证程序，并生成详细的综合报告。lxK一点就转

Certik基金会的工作由耶鲁和哥伦比亚大学三位教授主持.核心团队官网公布的信息也必将少，但在白皮书中提到将雇用至少20位软件工程师和科学研究人员。lxK一点就转