“You don’t want innovation to give someone a loophole to manipulate the system. We can help blockchain realize the promise that it was designed for.”

— Ronghui Gu, Assistant Professor at Columbia University, co-founder of CertiK

New York, New York Last year, IBM partnered with Columbia University to establish The Columbia-IBM Center for Blockchain and Data Transparency, a joint effort to facilitate innovation, education, and research in the field. With a history of collaborating that has spanned over 70 years, IBM and Columbia University embarked in another important milestone to demonstrate the continued commitment to research.

Garud Lyengar, a research leader at Columbia University, recently announced three projects that have been awarded with the Columbia-IBM Research Seed Funds. Among these projects is “The DeepSEA Framework for Building Certified Smart Contracts,” which aims to enable Formal Verification of smart contracts in Hyperledger Burrow by automatically generating machine-checkable, mathematical proofs. The DeepSEA program language will allow developers to implement smart contracts in a high-level language, while compiling into the bytecode of Hyperledger with a proof that no bugs are introduced during compilation.

DeepSEA has been spearheaded by Professor Ronghui Gu, who is also the cofounder of CertiK, the leading blockchain security company, which provides a full suite of cybersecurity services, including smart contract audits and penetration testing. CertiK leverages Formal Verification to provide an objective, mathematical approach to security, supplementing traditional methods of manual auditing. Currently, CertiK has secured over $1.2B in assets, verifying over 150 projects across all major protocols and establishing partnerships with popular cryptocurrency exchanges, including Binance, Huobi, and OKEx.

The advent of blockchain has propelled the usage of self-executing smart contracts, which are programs that can digitally facilitate, verify, and enforce the outcomes of a contract. However, because smart contracts have the ability to transfer users’ digital assets, these programs have become the focal points of malicious attacks. With an estimated $1B of cryptocurrency funds stolen in 2018, blockchain projects have been yearning for more rigorous means of verifying security.

Formal Verification uses mathematics to verify the correctness of a system with respect to its exact specifications. This rigorous approach has been more commonly used in mission critical hardware applications, from aerospace equipment to networking infrastructure, but the open-sourced nature of blockchain applications, as well as the direct access to users’ funds, has underscored the importance of Formal Verification of software. The DeepSEA research project examines how Formal Verification methods can be applied to smart contracts as a way to verify security and correctness, while limiting the changes in existing coding practices.

Professor Gu added that he is thankful for the Columbia-IBM Seed Funds grant that he received, which will allow him to work with a team of doctoral students to develop the DeepSEA-Blockchain platform. He intends to partner with researchers at IBM to determine the most impactful integration of the DeepSEA language and the Hyperledger platform. “The DeepSEA-Blockchain platform will allow developers to define specifications associated with contracts,” said Gu. “Developers can use the platform to customize contracts and add features that safeguard their currencies. They can add specifications such as ‘my money will never decrease in value or disappear,’ and the platform can ensure that the code satisfies the developer’s specifications. We appreciate the support from IBM and will continue our unwavering commitment to secure the blockchain ecosystem.”

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.