项目介绍：

CertiK是一个正式的验证框架，用于在数学上证明智能合约和区块链生态系统是无缺陷和抵御黑客的。为了扩展验证，CertiK开发了一种基于图层的方法来将这种验证任务分解的更小。这些较小的证明任务可以在CertiK交易中编码，然后由参与者以分散的方式证明和验证。因此，CertiK分类账本作为证书展示经过验证的智能合约和经过验证的区块链生态系统的端到端正确性和安全性，使其完全值得信赖。

项目介绍：

CertiK是一个正式的验证框架，用于在数学上证明智能合约和区块链生态系统是无缺陷和抵御黑客的。为了扩展验证，CertiK开发了一种基于图层的方法来将这种验证任务分解的更小。这些较小的证明任务可以在CertiK交易中编码，然后由参与者以分散的方式证明和验证。因此，CertiK分类账本作为证书展示经过验证的智能合约和经过验证的区块链生态系统的端到端正确性和安全性，使其完全值得信赖。

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

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

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

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

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

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

技术特点：

CertiK用形式化验证为智能合约和区块链应用提供代码安全服务。通过将智能合约转化为数学模型，并用逻辑上的推理演算来验证模型，从而证明智能合约的安全性。因为整个演算过程符合严谨缜密的数学逻辑，所以CertiK检验过的结果很难被黑客攻克。

CertiK核心产品基于CertiKOS防黑客操作系统演变迭代而来，这套系统历经两位创始人邵中教授与顾荣辉教授多年研究，并投入了千万美金的科研经费，其成果也被应用于军事级别软件系统的原型设计开发之中。

为了使验证过程具有可扩展性，CertiK通过将复杂的智能合约结构分层与模块拆分，可以使耗时耗算力的验证过程分解为更小更简单的任务。通过这种方式，CertiK分类账本就可以充当证书，以确保端到端的正确性——验证智能契约和块链的安全性——从而产生一个完全可信和安全的生态系统。

区块链关联度：

CertiK技术链

CertiK团队使用选定的DApps手动构建的经认证的DApp库。该基金会打算应用深度学习技术来建立一个智能标签框架。有了这个框架，大多数共享逻辑和属性都可以自动贴上标签，以便规范和证明工作可以戏剧性地进行降低。

CertiK证明引擎。带标签的程序将在内部编译，开发了CertiK编译器。CertiK编译器与通用编译器不同，识别标签语言，并可将标记的程序解析为内部模型为DApps。这个模型可以被看作是抽象自动机，定义DApp将如何更改系统状态（由所有全局变量和局部变量组成）。这个模型是语言独立的，因此证明引擎的后端可以统一。

发展路线：

CertiK团队使用选定的DApps手动构建的经认证的DApp库。该基金会打算应用深度学习技术来建立一个智能标签框架。有了这个框架，大多数共享逻辑和属性都可以自动贴上标签，以便规范和证明工作可以戏剧性地进行降低。CertiK证明引擎。带标签的程序将在内部编译，开发了CertiK编译器。CertiK编译器与通用编译器不同，识别标签语言，并可将标记的程序解析为内部模型为DApps。这个模型可以被看作是抽象自动机，定义DApp将如何更改系统状态（由所有全局变量和局部变量组成）。这个模型是语言独立的，因此证明引擎的后端可以统一。发展路线：​

2017年12月——CertiK的概念证明平台的技术和社区

2018年2月——基金会计划推出Alpha版CertiK智能标签和分层验证技术

2018年4月——推出CertiK平台的测试版

2018年6月——各种伙伴关系将进一步扩大，最终达到至少20个合作伙伴

商业模式：

CertiK的商业模式分两步走：

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

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

战略合作及投资机构：

据悉，CertiK已获耶鲁大学，丹华资本，光速中国等机构种子轮融资（金额暂未透露）；目前已与Neo、量子链等机构达成战略合作。

核心团队：

Ronghui Gu（联合创始人）

哥伦比亚大学计算机科学系的终身助理教授，并且获得了博士学位。他于2016年在耶鲁大学获得计算机科学硕士学位，他的论文获得了耶鲁大学杰出论文奖，并被提名为ACM论文奖。他于2011年获得清华大学学士学位。顾教授是系统软件正式验证方面的专家。他是CertiKOS的首席设计师和开发人员，CertiKOS是全球首个经过充分验证的并行操作系统内核。他在CertiKOS上的OSDI16论文已被提名并入选CACM的研究亮点部分。

Prof. Zhong Shao（联合创始人）

耶鲁大学计算机科学系Thomas L. Kempner教授和系主任。并且获得博士学位。他于1994年在普林斯顿大学获得计算机科学学位。在他早期的职业生涯中，他是SML / NJ编译器的主要开发人员，也是FLINT认证基础架构的主要架构师。近年来，一直是网络安全，编程语言，操作系统和认证软件等高度可见研究领域的领军人物。他在耶鲁大学的FLINT小组开发了世界上第一个耐黑客并发操作系统CertiKOS--这是建立可以免于软件漏洞的网络物理系统的一个重要里程碑。

VilhelmSjöberg（研究科学家）

耶鲁大学的副研究科学家，并且获得了博士学位。他于2015年在宾夕法尼亚大学获得计算机科学硕士学位。他是软件验证，编程语言和类型系统方面的专家。他的论文研究集中在使依赖型系统对通用编程语言更具吸引力，因为通过证明函数终止以及通过合并闭包来引入自动定理证明是可选的。目前他对CertiKOS等分层认证系统的语言支持感兴趣。Sjöberg博士是2016 ACM SIGPLAN John C. Reynolds博士论文奖的获得者。

项目热度：

1.Twitter：关注人数791，总推文11

2.YouTube：订阅者132

3.Telegram： 官方社区人数20777 

好了，以上就是对CertiK项目的分析，诸位看官，如果有好的分析建议可以随时联系小编，也请看官们给小编多推荐一些项目。