DeepSEA

书写可验证智能合约的语言

概述

形式化验证是一个强大的方法,从数学上确保程序能够正确和安全地执行,但是正因着它如此严密,它也有着极其消耗人力资源的特点。形式化验证最适用的场景是那些以高抽象级别书写,且支持方程式推理的程序,这样的程序可分解为独立的可验证模块。

为解决上述问题,CertiK正在开发一款名为DeepSEA的编程语言。这个语言是基于之前在耶鲁大学的一项由哥伦比亚-IBM区块链中心,哥伦比亚数据科学中心,Qtum基金会和以太坊基金会联合赞助的研究。由DeepSEA书写的程序将能够自动产生可执行的验证代码和一个可被载入Coq定理验证器的形式化模型。此模型可理解为由用户所书写的高抽象级别程序的一个输出。

上手试用

合作伙伴

  • icon
  • icon
  • icon
  • icon