CertiK是一個是形式化驗證框架，為智能合約和區(qū)塊鏈應用提供最先進安全性服務的公司。經(jīng)過CerTIK驗證的智能合同、DApp以及區(qū)塊鏈將會被附上證書形式的標志，來展示其正確性和安全性。

形式化驗證（Formal VerificaTIon）：用邏輯語言來描述規(guī)范，通過嚴謹?shù)臄?shù)學推演來檢查給定的系統(tǒng)是否滿足要求。

市場需求：安全是區(qū)塊鏈世界心中的痛

智能合約的出現(xiàn)使得區(qū)塊鏈進入了2.0的發(fā)展階段，盡管智能合約的發(fā)展十分迅猛，然而智能合約漏洞所導致的很多安全問題卻給人們帶來巨大的財產(chǎn)損失。眾所周知，公鏈系統(tǒng)基于信任和開放，一旦部署就是不可更改的。因此任何錯誤都很容易遭受黑客的攻擊。

2016年黑客通過The Dao，利用智能合約中的漏洞，成功盜取360萬以太幣。The DAO事件發(fā)生后，以太坊創(chuàng)始人Vitalik Buterin提議修改以太坊代碼，對以太坊區(qū)塊鏈實施硬分叉，將黑客盜取資金的交易記錄回滾，在得到社區(qū)大部分礦工支持的同時也遭到了少數(shù)人的強烈反對，最終導致了以太坊社區(qū)的分裂。

軍用級別的CerTIK 系統(tǒng)如何運行？

CerTIK區(qū)塊鏈解決方案是在已成功應用的技術基礎上開發(fā)的。CertiKOS是邵中教授領導的小組成功研發(fā)的世界上第一個反黑客攻擊操作系統(tǒng)，這個系統(tǒng)共花費千萬美元的科研經(jīng)費，兩位創(chuàng)始人邵中教授和顧榮輝教授用6年多時間研究安全系統(tǒng)，目前CertiKOS不僅在商業(yè)市場中通過驗證，也被應用到軍事防御系統(tǒng)上，并引起了耶魯大學等美國學術界的關注。

軍用級別的技術應用在區(qū)塊鏈和智能合約安全性，是不是聽起來很高大上，很復雜？其實CertiK客戶端的使用非常簡單，用戶可以一鍵提交并可接收檢測結果。

完整的驗證過程運作流程如下：

· 首先，客戶在客戶端向CertiK網(wǎng)絡提交智能合約或任何其他系統(tǒng)源代碼。

· CertiK將代碼的“正確性”轉換為類似的數(shù)學問題，然后以化整為零的解題思想，將一個難以證明的大問題拆分為許多容易證明的小問題，并將這些問題廣播到CertiK網(wǎng)絡。

· 分布式的CertiK節(jié)點并開始協(xié)作解決這些數(shù)學問題，以此換取獎勵。

· 節(jié)點把各自找到的解決方案反饋到CertiK區(qū)塊鏈上，并可以隨時被用于驗證。

· CertiK再將證明過的小問題重新組合回分解之前的較難的大問題，并將這些解決方案總結，并以證書的方式發(fā)送回客戶端。

· 這個證書將想客戶確認，要么代碼是安全的（無漏洞并課抵抗黑客），要么會支持潛在的風險和漏洞。

· 如果檢測出潛在的風險或者漏洞，CertiK會同時提供一些案例介紹這些風險或漏洞可能被攻擊的潛在方式。

全明星團隊配置：

CertiK由來自哥倫比亞和耶魯?shù)娜餍强茖W家團隊創(chuàng)建，并得到谷歌，F(xiàn)acebook和FreeWheel的高級軟件工程師的支持。

該團隊成立于硅谷和紐約市，由世界級的正式驗證專家組成，他們是耶魯大學計算機科學系教授邵中及其弟子、哥倫比亞大學計算機系助理教授顧榮輝。

邵中教授：

團隊聯(lián)合創(chuàng)始人，1988年本科畢業(yè)于中國科學技術大學，1989年至1994年就讀于美國普林斯頓大學，獲得計算機科學專業(yè)博士學位，1994年至今一直任教于耶魯大學，目前是計算機科學系的教授和系主任。他是SML / NJ編譯器的主要開發(fā)人員，也是FLINT認證基礎架構的主要架構師。

顧榮輝教授：

團隊創(chuàng)始人，2011年本科畢業(yè)于清華大學，計算機科學專業(yè)，2011年-2016年就讀于耶魯大學，獲得計算機科學專業(yè)博士學位，現(xiàn)任哥倫比亞大學計算機科學系的助理教授。他是CertiKOS的主要設計者和開發(fā)者，CertiKOS是世界上第一個經(jīng)過全面驗證的并發(fā)操作系統(tǒng)內核。

Vilhelm Sj?berg：

白皮書中展示的第三位成員，2015年獲得賓夕法尼亞大學計算機博士，主要研究興趣是軟件驗證，編程語言，類型系統(tǒng)和邏輯。

這個創(chuàng)始團隊得到了Google，F(xiàn)acebook和FreeWheel的高級軟件工程師的支持。該團隊目前正在擴展到最多20名軟件工程師和研究科學家，以便提供積極的路線圖。

發(fā)展路線圖 roadmap：

CertiK在過去幾年取得了實質性的進展，如下圖顯示的2015年至2017年間的發(fā)展取得了很大的成功：

那么CertiK的未來會怎么發(fā)展呢？

概念證明已于2017年12月開始，進展十分迅速。

alpha智能標簽和分層驗證產(chǎn)品已于2018年2月推出，CertiK團隊建立的在線社區(qū)正在進行測試和改進。

2018年5月推出了測試版產(chǎn)品，并與數(shù)家商業(yè)合作伙伴建立合作。2018年6月首次發(fā)布CertiK1.0產(chǎn)品，并與30家商業(yè)合作伙伴進行合作計劃于2018年下半年全面對外公開產(chǎn)品服務。

都有誰看好CertiK？

CertiK已獲得幣安實驗室、耶魯大學、丹華資本、光速中國等機構的支持；

同時CertiK將為Qtum量子鏈提供全棧式的形式化驗證服務，包括提供Qtum系Dapps的安全性報告與一站式驗證服務，為Qtum X86虛擬機的形式化建模 （formal model），以及Qtum量子鏈的代碼證明等，為Qtum生態(tài)系統(tǒng)的安全性保駕護航。除此之外，菩提、Ink、nebulas星云鏈也和CertiK建立了合作關系。