CertiK

DeepSEA/Blockchain—A language to write verified Ethereum contracts

Overview

Formal verification is the most powerful method for ensuring that programs work correctly and securely, but it remains very expensive. Part of the problem is that current programming languages do not provide good support for writing verified system software. To get good runtime performance and interoperability one wants detailed control over data representation, but formal verification works best when programs are written at a high abstraction level and support equational reasoning, and large systems must be decomposed into modules that can be verified separately.

Prior and ongoing work at Yale University is developing the DeepSEA programming language, which aims to ease the work on verification by automatically generating both executable code, and a formal model of the code which can be loaded into the Coq theorem prover. The model is in the form of a functional program, at a higher level of abstraction, and furthermore the style of abstraction layers.

The DeepSEA language was originally designed for implementing system software such as OS kernels, but the same set of features that are used for encapsulating state inside a kernel is also very suitable for implementing smart contracts. CertiK is now developing a port DeepSEA to work on blockchain. This will take the form of a verifying compiler from DeepSEA to Ethereum contracts, which will let the user reason about the contract in a proof assistant at a high level of abstraction, while still generating trustworthy code.

People

The following people are involved with the project, or have been in the past.