CertiK Chain對DeepSEA的支援
DeepSEA非常獨特。和其他程式語言不同的是，它是被專門設計用來編寫可認證的正確程式碼的。
今天，幾乎所有的智慧合約都是用未被設計支援形式化驗證的語言寫出來的。即使那些支援形式化驗證的語言，也只是針對一些簡單的情況。
DeepSEA則利用了互動式高階邏輯輔助定理證明工具，從而能夠對諸如跨鏈、投票這樣的複雜程式進行靈活的證明。DeepSEA的編譯器不僅能生成可執行的位元組碼，同時還能生成和這些位元組碼對應的可形式化驗證的模型，從而使得這些程式碼在數學意義上的正確性可以由開發者們用輔助定理證明工具驗證。
如果你想了解有關DeepSEA的更多資訊，可以檢視之前的文章【宅在家裡最適合看的程式設計，C++、Java還是……沈從文？】以及【2020最具“戰略性”的程式語言：C語言？還是C# 、 Python 、Swift？】來了解。
透過對DeepSEA的整合，CertiK Chain能夠不折不扣地將安全作為第一要務。在使用DeepSEA寫智慧合約時，部署者（或其他使用者）可以基於編譯器的輸出構造出關於程式正確性的證明，並且將其推送到鏈上。接下來證明將會得到檢驗，並被髮表，從而完成對於合約的認證。長遠而言，使用者和合約都可以根據某合約的認證及相關證明資訊而決定是否與其進行互動。
與以太坊虛擬機器（EVM）相容的位元組碼
DeepSEA編譯器有一個經過驗證的後端來生成與以太坊虛擬機器（EVM）相容的位元組碼。而這些位元組碼和Solidity的二進位制應用介面（ABI）也同樣相容。所以任何使用Solidity編寫的合約都可以呼叫使用DeepSEA寫的合約，反之亦然。
DeepSEA程式可以被部署到以太坊之上。但由於CertiKChain的虛擬機器（CVM）也和EVM相容，它們也能在CertiK · Chain上執行。重要的是，與傳統的以太坊合約不同，在CertiK Chain上執行的DeepSEA合約有一些額外的能力：
· CertiK Chain支援記錄一個程式是否透過形式化驗證滿足了特定形式化規範
· 合約在執行時可以查詢特定地址上的合約是否滿足特定規範
DeepSEA編譯器會輸出用高階邏輯表述的程式碼規範，並且其可以在鏈上被註冊。DeepSEA程式也可以查詢特定地址是否被形式化驗證過。例如，這將能夠讓程式只與那些已經證明沒有回撥（callback-free）的合約互動。
證明的區塊鏈
在以上的系統中，每個使用者只有兩個選項：要麼自己檢查一遍證明，要麼相信一個第三方來檢查。然而，這兩者都有可能出錯，因為這需要非常熟悉證明工具以及相關的庫，以確保沒有誤用任何錯誤的假設。除此之外，智慧合約在執行時仍然無法查詢證明。
為了解決這個問題，CertiK Chain將把證明的檢驗作為鏈的核心功能之一。一段冗長的證明可以被切分成很多小段，而每一小段證明都會被多個驗證節點（verifier node）檢查。當所有的驗證節點就一段證明的正確性達成了共識，證明所對應的定理將被寫入鏈的下一個區塊，記錄為已證明。
這意味著CertiK Chain將會建立世界第一個記錄已驗證宣告的共識機制。每當一個新的定理被寫入鏈中，所有人都能精確瞭解這個定理做出了哪些假設。所有使用者都可以在自己的形式化驗證的開發中，放心地使用此定理，而智慧合約則也可以在執行時隨時進行定理的證明查詢。
DeepSEA的部署與互動
DeepSEA可以直接透過命令列工具CLI部署，也可以透過DeepWallet網頁介面來進行。
CLI會呼叫DeepSEA的編譯器，然後獲取生成的位元組碼和二進位制應用介面（ABI）。部署一個DeepSEA合約和部署一個Solidity合約一樣，他們使用同樣的命令，非常簡潔：
certikcli tx cvm deploy <ckt><filename>
開發者們也可以自行編譯位元組碼（以及ABI，如果想要的話），把位元組碼存到一個檔案裡，然後使用同上的命令來部署（如果有ABI的話再加上--abi的flag）。使用DeepSEA和Solidity部署的函式都可以被同樣的命令呼叫：
certikcli tx cvm call <address><ckt> <function>
DeepSEA也可以透過DeepWallet部署。DeepWallet是一個允許使用者傳送、收取、以及質押CTK的安全錢包應用，同時，它還支援使用DeepSEA（以及Solidity）開發、部署、使用安全智慧合約於CertiK Chain之上。透過DeepWallet友好的使用者介面，使用者可以直接與DeepSEA互動。
構建安全區塊鏈生態的無限可能
安全顯然是任何區塊鏈系統實現透明及信任的基礎。正是因為區塊鏈的安全要求如此之高，這些要求最終只可能被可機器檢查的安全數學證明所滿足。
DeepSEA的開發工作部分由哥倫比亞-IBM區塊鏈中心和以太坊基金會資金支援。DeepSEA以任何其它語言都無法企及的安全性讓我們距離構建安全區塊鏈生態系統的願景更近了一步。CertiK Chain和DeepSEA的整合讓所有的區塊鏈使用者都將能在終極的信任和證明的基礎之上開發全新的殺手級應用，以天馬行空的想象力築建安全區塊鏈生態的無限可能。
