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

形式化驗證（Formal Verification）：用邏輯語言來描述規范，通過嚴謹的數學推演來檢查給定的系統是否滿足要求。

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

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

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

軍用級別的CertiK 系統如何運行？

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

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

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

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

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

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

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

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

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

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

全明星團隊配置：

CertiK由來自哥倫比亞和耶魯的全明星科學家團隊創建，并得到谷歌，Facebook和FreeWheel的高級軟件工程師的支持。

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

邵中教授：

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

顧榮輝教授：

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

Vilhelm Sj?berg：

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

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

發展路線圖 roadmap：

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

那么CertiK的未來會怎么發展呢？

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

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

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

都有誰看好CertiK？

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

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