DeepSEA intends to create a bug-free & hacker-resistant blockchain infrastructure by implementing verifiable smart contracts
Smart contract languages are basically used to write executable code on blockchains. The most well known in this regard is Solidity — a programming language designed for developing smart contracts that run on the Ethereum Virtual Machine. Ethereum as most of you know is the pioneer blockchain when it comes to deploying smart contracts. More recently, Facebook’s project Libra also launched its own smart contract language by the name of the Move.
However, there is an inherent drawback with the current smart contract languages — there is no process dedicated to the formal verification of the complex & executable only code. Blockchain systems are based on the foundation of trust and consensus protocols alone can’t keep them trustworthy. Program bugs in the code or malicious intervention by hackers can easily derail this process.
This is what the new DeepSEA programming language intends to fix. The endeavor backed by Binance Labs, the Ethereum Foundation & Qtum was originally created by Professor Zhong Shao, department chair of computer science at Yale and the co-founder of Certik, together with Ronghui Gu, an assistant professor of computer science at Columbia University.
The earlier mandate of DeepSEA only included the limited capability of implementing system software, which has now been transitioned into taking up the more challenging task of formal verification and audit of smart contracts and blockchain protocols. Researchers have argued this was required to address the smart contract vulnerabilities that most of the existing languages are ill-suited to handle.
In the next-generation digitized systems where software code is the king, it is imperative that we have air-tight procedures like Formal Verification in place to mathematically check that the code works as it is intended to do so. Existing tools work well with simple contracts but complex contracts like voting schemes or cross-chain interactions need Formal Verification.
Unlike most of the current programming languages, DeepSEA comes integrated with the Formal Verification system. The language is designed to support the best features of other programming languages and constitutes of the following four principles.
❶ Equational Reasoning — DeepSEA terms are translated into corresponding functional specifications.
❷ Layered Specification — Proofs are managed by abstraction layers that provide a high-level view of the program.
❸ Encapsulation and Composition — Multi-layer architecture which houses objects which can be verified periodically.
❹ Built-In Abstract Refinement — User-friendly verification of larger, more complex systems.
Other solutions like Ricardian contracts also aim to improve on the limitations of the smart contracts by converting human-readable legal contract between multiple parties into machine-readable software code which can be executed with all the features of the smart contract. For now, CertiK has released a demo and language reference manual.
To download the DeepSEA manual & compiler and technical details can be accessed here.
Medium | Twitter | LinkedIn | StockTwits | Telegram
