DeepSEA编程语言的目标是使用Coq定理证明助手去从头到尾的验证合约的正确性。DeepSEA系统语言的组成部分有：一个新的编程语言，一个已被验证的编译器，和一个能将合约代码翻译成可被Coq证明助手加载的形式化模型的编译机制

　　CertiK正在开发一个经验证的编译器，该编译器可以将DeepSEA语言翻译成字节码。由于编译器本身已经通过了Coq辅助证明工具的验证，该编译器不存在任何可能破坏合约安全属性的漏洞。换句话来说，用户不仅可以在源代码层面证明程序的安全性，并且这个安全性和用户直接使用字节码的形式化规范进行推理得出的安全保障一样严格可靠。并且，由于验证证明不会有大量控制流或者数据表示的问题，整个证明过程将会变得更为便捷。而编译器通过了安全验证这一事实也意味着所有通过编译的程序都满足某些运行时安全性质，并且这些性质是可验证的，比如：类型安全、没有整数溢出，等等。

　　DeepSEA是一个模块化的系统，因此DeepSEA变成语言可以被编译到不同的目标架构中，并且经过验证的编译器后端可以被不同的前端语言重复使用。在未来，团队可以将这些后端重新用于领域特定语言（DSL）上（例如特别用于开发金融合约的语言），而这些DSL都可以拥有和其他语言相同的正确保障。

　　DeepSEA编译器会将合约翻译到一个可被加载到辅助证明工具中的库中，在那里将会执行对于高级的正确属性的证明。能够使用功能完整的交互式证明助手意味着用户可以定义任意复杂定理的陈述和模型，并且不会被证明工具本身的限制所影响。举个例子，当证明一个金融程序的时候，用户可以写出一些博弈论的定义（就像数学书里面一样）并证明预期协议确实是一个占优策略。

　　另外一个例子也能够证明辅助证明助手的功能非常强大：跨链应用。跨链应用包含了很多存在于不同的链上的并且进行异步通信的智能合约上。这是另外一个DeepSEA能够为OKChain生态赋能的好方式。在这个环境下，DeepSEA工具可以针对每个单独合约自动输出一个经过验证的模型，然后开发人员可以使用辅助证明助手去定义该智能合约怎样与别的合约进行交互，改对延迟进行怎样的假设等等。DeepSEA可以被编译到不同的链上运行，比如说CertiK Chain，OKChain，Ethereum，这也同样可以为用户写一套标准的用于桥接的合约提供帮助，然后在一个单独的DeepSEA开发中将它们全部验证，为跨链交流提供坚实基础。

　　 (责任编辑：admin1)