The beneficiary of the grant is a smart contract R&D project called DeepSea, spearheaded by Professor Ronghui Gu, an assistant professor of computer science at Columbia, in collaboration with researchers at Yale. Gu is also the co-founder of blockchain security firm CertiK, which is also one of the participants in the project that raised “several millions” in a funding round led by Binance Labs last October.
DeepSea is named after a new smart contracts programming language, originally created at the research lab of Professor Shao, department chair of computer science at Yale and Gu’s fellow co-founder at CertiK.
While the language was initially designed for the implementation of system software, the press release notes that the high risks surrounding smart contract vulnerabilities have provided a fresh impetus to extend DeepSea’s “protective features” to that arena. As Professor Gu has outlined:
“Because [smart] 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 refers to “the process of leveraging mathematical proofs to verify the correctness of code implementation,” and was reportedly initially implemented in the NASA Mars Rover and other hardware systems that the press release characterizes as “mission critical.”
The process is now reportedly being extended for use in software systems, as with CertiK’s auditing of smart contracts and blockchain protocols, and can be used to prevent the possible introduction of bugs while compiling DeepSea into the EVM.