Check out our DeepSEA research page for the latest updates!

In the blockchain world, security is paramount, but writing certifiably correct system software is quite labor-intensive. Current programming languages are not well-suited for the task—let alone compatible—with Formal Verification.

Enter DeepSEA: the new language to write verified Smart Contracts. Let’s dive into the details.

What is DeepSEA and Why Was It Built?

DeepSEA is a language that allows programs to handle extremely complex code while operating elegantly and securely for the coders themselves. It is designed to be useful when doing full Formal Verification in the Coq system, a proof assistant.

Formal Verification mathematically proves code will work as intended, computing all possible scenarios. And as pioneers of Formal Verification technology on smart contracts and blockchains, CertiK found that although formally verifying software was the only way to objectively show immunity against vulnerabilities, writing fully-correct software remained very expensive and challenging.

Part of the problem is due to the lack of programming language support. Existing languages, like C or OCaml or Solidity, are not well integrated with the verification tools and require time to create and prove manual proofs. However, the DeepSEA language provides a way to formally verify difficult correctness properties about smart contracts using the Coq Proof Assistant in a scalable and automated way.

Assuming that much of a developer’s time is spent writing proofs in an interactive proof assistant, such as Coq, DeepSEA aims to remove as much busy-work as possible and help developers structure their system into separate modules so that the rest of the system contains verified air-tight proofs.

How Is It Built?

When designing the language, we used four principles that combines the best features of several other programming languages:

Equational Reasoning: Each DeepSEA term is translated into a corresponding functional specification, which can then be reasoned about in the Coq proof assistant.

Layered Specification: DeepSEA keeps proofs manageable by abstraction layers which provide a high-level view of the program. The compiler proves that the raw bytecode implementation behaves as intended, while the programmer only needs to look at the high-level representation.

Encapsulation and Composition: Each DeepSEA layer consists of a set of objects that are built on top of another layer, and the layers can be proven correct one at a time.

Built-In Abstract Refinement: DeepSEA verifies larger systems in user-friendly steps. The process is structured as a series of linked refinement proofs that prove that a linked program meets the specification.

Why Does This All Matter?

Blockchain ecosystems are built on the foundations of trust. While some argue that consensus protocols are what makes blockchains trustworthy, some codes are still not truly trustworthy due to program bugs and malicious hackers.

For example, if a particular function in your smart contract overflows -- that’s a problem. If a function implementation does not meet the specifications and leads to (un)intentional vulnerabilities -- that’s a problem.

Then what? If you move trust from people to programs, then the program needs to be trustworthy. This requirement is important in blockchain because once a smart contract is deployed, there is no easy way to undo it, leaving undetected vulnerabilities open to exploitation.

Formal Verification is the only reliable way to make sure code is air-tight and checked against unequivocal mathematical facts. By proving that the program handles every possible input value correctly, it mathematically ensures that the code works only as it’s intended to. And in all the cases where Formal Verification is applied, DeepSEA allows developers to prove an arbitrary number of complex contracts.

Contracts range from simple to complex, and so does Formal Verification. Existing automatic tools deal well with very simple contracts such as tokens. However, in order to verify complex contracts like voting schemes or cross-chain interactions, we need the flexibility to define arbitrarily complicated specifications and proofs.

This is where interactive proof assistants like Coq shine. By integrating smart contracts and Coq we can apply Formal Verification to the most challenging tasks, allowing for a completely verified system end-to-end.

Are there other languages that support this?

Today, nearly all contracts are written in programming languages which were designed without Formal Verification in mind. Even when they do integrate with a Formal Verification system, they are usually geared towards automatically dealing with simple cases.

The built-in Solidity SMT solver is one good example. The SMT solver allows programmers to annotate a function with conditions that are assumed to be true, write assertions that should hold, and ask the compiler to prove them automatically.

However the assertions are limited to a fixed vocabulary (about numbers and arrays) and can only talk about the state of a program during a particular single method call. That is, the solver can only prove the assertion, and not other kinds of theorems. Similarly, the user has to trust that the compiler itself is not buggy.

More ambitious verification systems, for example the K framework, remove some of these issues by using a formal specification of the EVM and by letting the programmer do more of the manual work (e.g. supplying loop invariants). However, these verification systems lack abstraction from the bytecode and still only focus on single-run properties with a fixed vocabulary.

To get enough power to verify arbitrarily complicated properties we want to use an interactive proof assistant like Coq or Isabelle. Although interactive proof assistants have built-in programming languages, they compile via functional programming languages that use garbage collectors (automatic memory collectors).

In the context of blockchain, having a garbage collector makes smart contracts slow and expensive since it requires gas. So the built-in language of Coq is not directly usable for Ethereum. Fortunately, the DeepSEA compiler bridges this gap by generating both efficient executable code (which can run without a garbage collector) and a formal model which can be loaded into Coq.

DeepSEA is a flexible and compatible language that can create fundamental and intuitive design with a high level of abstraction and reasoning using Coq. We believe that—with next-generation technology—comes next-generation security. DeepSEA provides an elegant solution to secure code ––sharper, stronger, and more efficient than ever.

To learn more and get the latest updates about DeepSEA, check out our DeepSEA research page.

If any questions, feel free to email us at marketing@certik.io