「Certik」是一家用形式化驗證技術保護智慧合約和區塊鏈生態的安全的驗證平臺，致力於應用形式化驗證技術，為智慧合約和區塊鏈生態提供安全保護。

CertiK的核心產品是CertiKOS防黑客作業系統，採用了形式化的驗證 (formal
verification)，將智慧合約轉化為數學模型，通過邏輯上的推理演算來驗證模型，從而證明智慧合約的安全性。

這個系統共花費千萬美元的科研經費，兩位創始人邵中和顧榮輝用6年多研究安全系統，目前CertiKOS不僅在商業市場中通過驗證，也被應用到軍事防禦系統上，並引起了耶魯大學等美國學術界的關注。

CertiK的商業模式分兩步走：

1、依靠CertiK自身算力的中心化驗證服務。如果客戶本身有強大的硬體裝置和系統，可向CertiK提交智慧合約和需求，CertiK將合約轉化為數學模型，進行形式化驗證，並生成報告，指明合約中哪一行可能出現漏洞，系統在什麼狀態或條件下可能被侵入(具體步驟可參考demo演示)。CertiK根據合約的複雜程度收取不同的服務費。

2、去中心化的安全驗證生態系統，藉助社群參與者的算力，共同生成報告。前文提到的分層結構理論可將複雜任務拆分成小的模組，CertiK接到客戶需求後，將“任務”和技術工具分發給社群，獎勵提供算力、幫助檢驗小型模組的貢獻者。交叉驗證機制可以確保社群內無人投機取巧、沒完成任務還“騙取獎勵”。CertiK認為，這種任務分發要比算hash值挖礦更有意義、更低能耗。

CertiK平臺特色：

1、智慧標籤——CertiK平臺設計了一種新穎的方法來指定DApps
/系統使用標籤。這些標籤具有足夠的表現力，可以正式宣告期望的屬性並且與現有的程式語言相容(例如，密實度)。通過利用手動建立標籤的深度學習技術程式碼庫的培訓，CertiK平臺打算引入一個框架，命名為智慧標籤，不僅在語法層面理解分散式程式而且在語義層面上，可以自動向原始碼新增適當的標籤。

2、基於層的分解——
CertiK團隊是首批實現模組化的團隊之一，通過實現一種新的概念進行驗證，命名為分層深度規範。這種技術揭示了分層設計模式的見解並使其成為可能將複雜的證明任務分解成更小的模組，並在他們的每個人身上驗證他們適當的抽象層次。

3、可插入的驗證引擎——這些分解的證明義務更容易解決，甚至可以通過一些自動驗證器來解決。為了實現可擴充套件性，CertiK平臺旨在提供開放協議，這樣更高階的求解演算法可以自由地插入到這個系統中。

4、機器可檢驗的證明物件——
CertiK平臺構建機械化證明物件(或反例)，以便這些證明可以被任何人快速檢查使用自己的機器。這些證明物件可以被看作是“證書”到已驗證的程式。

5、認證的DApp庫——為了提高整個區塊鏈社群程式碼的質量和可靠性，CertiK平臺提供了一系列認證庫和外掛整合開發環境(IDE)以構建更多值得信賴的DApps。使用這些工具將花費少量的CTK虛擬加密“燃料”，但會在開發期間提供更多的保證。

6、定製認證服務——對於高可靠性的DApps
/系統(例如數字錢包)CertiK平臺有意提供定製認證服務。在這種情況下，驗證專家將幫助指定/驗證程式，並生成詳細的綜合報告。

Certik基金會的工作由耶魯和哥倫比亞大學三位教授主持.核心團隊官網公佈的資訊也必將少，但在白皮書中提到將僱用至少20位軟體工程師和科學研究人員。