Ethereum Foundation Awards Grant for DeepSEA Research by CertiK, Yale, and Columbia to Create Safer Smart Contracts

Ethereum Foundation Awards Grant for DeepSEA Research by CertiK, Yale, and Columbia to Create Safer Smart Contracts

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.

About CertiK

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 [email protected] or visit certik.io to submit your request today.

Twitter: https://twitter.com/CertiKCommunity

Telegram: https://t.me/certikorg

Related Blogs

CertiK Hack3D: H1 2026 Report

CertiK Hack3D: H1 2026 Report

Web3 security losses exceeded $1.31 billion in H1 2026 across 344 incidents, with wallet compromise emerging as the most financially destructive attack vector and phishing shifting toward fewer, higher-value social engineering attacks.

Introducing CertiK Hunt, The Invite-Only Security Platform for Web3 Projects and Top Security Researchers

Introducing CertiK Hunt, The Invite-Only Security Platform for Web3 Projects and Top Security Researchers

CertiK Hunt is an invite-only platform connecting elite security researchers with web3 projects through bug bounty programs, audit competitions, and AI challenges.

What Are Decentralized Apps (dApps)?

What Are Decentralized Apps (dApps)?

Decentralized apps (dApps) run on blockchain networks like Ethereum, Solana, BSC, SUI, and Avalanche. Learn what dApps are, how they work, examples, and their advantages in Web3.