The Language to Write Verified Smart Contracts
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
Read More About DeepSEA
An Introduction to DeepSEA
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
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
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.