DeepSEA
书写可验证智能合约的语言
概述
形式化验证是一个强大的方法，从数学上确保程序能够正确和安全地执行，但是正因着它如此严密，它也有着极其消耗人力资源的特点。形式化验证最适用的场景是那些以高抽象级别书写，且支持方程式推理的程序，这样的程序可分解为独立的可验证模块。
为解决上述问题，CertiK正在开发一款名为DeepSEA的编程语言。这个语言是基于之前在耶鲁大学的一项由哥伦比亚-IBM区块链中心，哥伦比亚数据科学中心，Qtum基金会和以太坊基金会联合赞助的研究。由DeepSEA书写的程序将能够自动产生可执行的验证代码和一个可被载入Coq定理验证器的形式化模型。此模型可理解为由用户所书写的高抽象级别程序的一个输出。
上手试用
合作伙伴
了解更多DeepSEA
An Introduction to DeepSEA
Jan 10
In the blockchain world, security is paramount, but writing certifiably correct system software is quite labor-intensive. Current programming languages are not well-suited for the task—let alone compatible—with Formal Verification.
How DeepSEA Works
Jan 22
The DeepSEA language syntax is inspired by functional languages like ML and Coq itself. The simple token contract below shows the general appearance, we will use it as a running example.
Solidity vs Move vs DeepSEA
Jun 21
We compare Facebook’s Move with Ethereum’s Solidity and CertiK’s DeepSEA to interpret the differences between the languages, detailing the advantages — and complications — therein.