DeepSEA

The Language to Write Verified Smart Contracts

Overview

Formal Verification is a powerful method to mathematically ensure programs work correctly and securely, but it remains resource-intensive because of its rigor. Formal Verification works best when programs are written at a high abstraction level, support equational reasoning, and are decomposed into discrete modules that can be verified.

Building on prior work at Yale University with funding from Columbia-IBM Blockchain Center, Columbia Data Science Institute, Qtum Foundation, and Ethereum Foundation, CertiK is developing the DeepSEA programming language, which eases the work on verification by automatically generating executable code, as well as a formal model that can be loaded into the Coq theorem prover. The model is output as a functional program with a higher level of abstraction and in the style of abstraction layers.

Try It for Yourself

Made Possible By

  • icon
  • icon
  • icon
  • icon