DeepSEA CertiK Shentu 官方网站


官方网站: https://www.certik.foundation/

在今天的区块链中,智能合约安全的负担是严重片面的,要想知道 外部智能合约 或 功能 是否 足够安全,而不危及存储在区块链上的资产和信息,几乎是不可能的。

CertiK链将这一责任负担均衡化,为用户提供了一种更通用的方式,根据智能合约的安全程度来设定其智能合约应如何与他人交互的规则。

通过在CertiK链中构建这些保障措施,开发人员可以花更少的时间来保护他们的智能合约,而花更多的时间来构建可能性。

DeepSEA
编写验证智能合约的语言

https://certik.io/research/deepsea/

概述
形式化验证是一种强大的方法,可以从数学上确保程序正确安全地工作,但由于其严格性,它仍然是资源密集型的。

当程序以高抽象级别编写,支持方程推理,并被分解成可以验证的离散模块时,形式化验证效果最好。

在耶鲁大学之前的工作基础上,在哥伦比亚-IBM区块链中心、哥伦比亚数据科学研究所、Qtum基金会和Ethereum基金会的资助下,CertiK正在开发DeepSEA编程语言,通过自动生成可执行代码,以及可以加载到Coq定理推理器中的形式化模型,来减轻验证的工作。

该模型以抽象层的风格,以较高的抽象层次的函数程序形式输出。

https://github.com/certikfoundation/shentu

https://docs.certik.foundation/certik-chain/