Update: Check out our DeepSEA research page for the latest news!
New York, NY — March 6, 2019 — In the announcement of the 5th wave of research grants, the Ethereum Foundation awarded the DeepSEA project with a grant to compile the smart contract programming language directly into the Ethereum Virtual Machine (EVM). The Ethereum Foundation Grants Program is an ongoing effort to support critical Eth 2.0 and Layer 2 scaling efforts, with its prior wave of grants announced in mid-October 2018.
The DeepSEA project is spearheaded by Professor Ronghui Gu, Assistant Professor of Computer Science at Columbia University and co-founder of the blockchain security company, CertiK. A research project with collaborators of CertiK, Yale University, and Columbia University, the DeepSEA program language will allow programmers to implement smart contracts in a high-level language while using a Formally Verified compiler to ensure that no bugs are introduced during the compilation into the EVM.
The Ethereum Foundation grant marks the latest in a series of high-profile research grants awarded to the DeepSEA project. Earlier this year, IBM announced a research grant for the DeepSEA project to enable the Formal Verification of smart contracts on Hyperledger Burrow. In December 2018, the Qtum Foundation awarded $400k to the DeepSEA efforts of Professor Gu’s lab at Columbia University.
The DeepSEA language was initially developed at the research lab of Professor Shao, Department Chair of Computer Science at Yale University and co-founder of CertiK, and was originally designed to implement complex system software such as OS kernels. With clear consequences surrounding smart contract vulnerabilities, the implementation of smart contracts served as a suitable extension of the protective features of the DeepSEA language.
“Smart contracts play a pivotal role in unlocking the promise of blockchain,” says Prof. Gu. “Because these contracts are self-executable and permanent, it is crucial that these contracts perform only as they are precisely intended. The DeepSEA language will allow programmers to add safeguards to ensure that the code conforms exactly to its specifications, using Formal Verification.”
Formal Verification is the process of leveraging mathematical proofs to verify the correctness of code implementation. Used by the NASA Mars Rover and other mission-critical hardware systems, the adoption of Formal Verification in software systems has seen a surge with the advent of smart contracts. CertiK, which specializes in using Formal Verification to audit smart contracts and blockchain protocols, has secured over $1.2B in assets by verifying over 160 token projects, including BNB and TrueUSD. The company announced an investment led by Binance Labs last October, in which Ella Zhang, CEO of Binance Labs, highlighted CertiK’s ability to “bypass the limitations of manual detection.”
The recent research grants of the DeepSEA program language signal the proactive approach of limiting security vulnerabilities by advancing coding methods and the underlying technology.
To learn more and get the latest updates about DeepSEA, check out our DeepSEA research page.
CertiK is a blockchain and smart contract verification platform founded by top formal verification professors from Yale and Columbia University and former senior software engineers from Google and Facebook. Expanding upon traditional testing approaches, CertiK utilizes mathematical theorems to objectively prove that source code is hacker-resistant to some of the most critical vulnerabilities. With the mission of raising the standards of cybersecurity, CertiK is backed by prominent investors, including Binance Labs, Lightspeed, Matrix Partners, and DHVC.
To request the audit/verification of your smart contracts, please send email to firstname.lastname@example.org or visit certik.io to submit your request today.