We are the only team which provides
fully automatic exact verification technology with the following features:
All reported errors are real
All errors are detected
No need for human intervention
Allow arbitrary programs and provide formal guarantees
Continuous Smart Contract Verification: A security layer for smart contract
Modular Formal Verification: A contract development environment
Certora provides Formal Verification of Smart Contracts which is accessible and cost-efficient. Certora has unique technology called AEV (standing for Automatic Exact Verification) capable of checking all executions of a Smart Contract fulfill a set of requirements.
AEV technology is available as a tool that complements existing compilers and debuggers of Smart Contracts. It checks that the contracts fulfil its requirements and adheres to the interface requirements of other contracts. Certora’s blockchain independent and language-agnostic AEV technology precisely identifies bugs in Smart Contracts and proves their absence. Certora offers two unique solutions targeted for all participants in the blockchain ecosystem:
Continuous Smart Contract Formal Verification
(CFV) for businesses that employ Smart Contracts. CFV continuously monitors all contracts for newly
discovered vulnerabilities or changes that may expose new issues.
CFV guarantees long-term safety of your digital assets in the blockchain by notifying immediately on any new issues, thus reducing incident response time. This allows your business to avoid the consequences of undesired irreversible transactions.
Quality Development Environment
(QDE) for developers permits developers to detect issues during development, maximizing security by the
time of contract deployment.
QDE automatically produces a report of existing issues, reporting their severity and the exact manner in which they reproduce.
Certora AEV builds on 30 years of academic research and hundreds of academic publications which pioneeered the area of Formal Verification. The team combines academic leadership, industrial strength and Blockchain expertise.
Professor and a Chair of Software Systems in the School of Computer Science at Tel-Aviv University with 30 years of experience in formal methods and static code analysis. He contributed techniques which were integrated into the Microsoft device driver verification tool and Panaya ERP tool acquired by Infosys. He is also a co-designer of Ivy. He a fellow of ACM and a recipient of Microsoft Outstanding Award for contributions to formal methods. Sagiv is a recipient of the most prestigious European grant.
Blockchain enthusiast with background in Formal Verification. She is also an experienced software engineer which spent 5 years at Check Point. Shelly is the lead author of the isolation technique for ensuring the correctness of modular reasoning. She graduated from the Adi Lautman undergraduate excellence program and is a PhD candidate in Smart Contract Verification at Tel Aviv University.
Experienced software engineer with rich practical experience in software systems development at Elite Technological IDF Unit, Google and at Dell EMC. Acted as team leader and core team architect. He is the lead author behind the technique for modularly verifying distributed systems integrated into Ivy. He holds bachelor in Computer Science Cum Laude from the Technion Israel Institute of Technology
Formal verification expert with MSc in formal methods from the Technion Israel Institute of Technology under the supervision of Professor Orna Grumberg. He has been interested in Cryptocurrency right from the beginning. He has 20 years of experience in the hardware verification industry including IBM Haifa Research Labs and Marvell. He published 5 US patents and several scientific articles on formal verification.
Launching a first release of QDE, freely available.
Launch of Continuous Formal Verification service.
Yes. There are actually two difficult problems:
(1) How does one define what requirement to check
(2) Given a requirement, how to make sure that all executions of the program fulfill the requirement. The Certora proprietary technology, AEV (standing for Automatic Exact Verification), addresses the second problem. The second problem is especially interesting for software systems such as Smart Contracts, in which the number of potential states is infinite. This is realized in programs with loops and contracts which call each other. In fact, virtually all contracts have an infinite state since they are reactive.
Therefore, we develop unique technology which can reason about such programs in an accurate way.
Certora offers two mechanisms:
(1) A list of predefined requirements based on best practices defined by the Smart Contract community.
(2) The user defines requirements using a new command called 'ensures' which behaves similarly to Solidity's assert, but is checked at compile-time by the Certora AEV engine.
Certora optionally enforces a requirement which ensures that external contracts cannot change the internal state of the checked contract. This automatically prevents bugs like the DAO. It also enables Certora AEV to verify the code without considering the potentially complicated code of the external contract. Thus, Certora verifies one contract at a time. In the formal method community this is called rely-guarantee reasoning. This is similar to the notion of separate compilation in compilers.
A beta version of AEV will be publically available February 2019.
Certora facilitates trust by the combination of the following:
(1) Providing an executable tool where users can review the verification process and reproduce it at any point in time.
(2) Generating artifacts of the verification, which can be reviewed by non-experts without depending on Certora's tools. These artifacts are test inputs that demonstrate pathes in the code which lead to violations and satisfaction of requirements.
(3) Developing proprietary technology for automatically generating machine checkable proofs. In Computer Science, this area is called Proof-carrying code.
Smart contracts are vulnerable to so called "callback attacks".
The attacker contract can exploit the fact that the internal state of the
contract is not yet stable.
This happened in the
DAO attack and the
One way to avoid the problem is to limit the use of callbacks to occur in the last
command in the contract but this can be too restrictive in many cases.
Effectively Callback Freedom: We are enforcing a requirement which permits liberal usage of callbacks as long as the state of the contract cannot be manipulated in a way which breaks its correctness. For additional documentation, refer to:
- A short Video by Shelly Grossman
- A long Video by Noam Rinetzky taken at POPL'18 LA
- Academic Paper
- Technical Report
Acknowledgements This is a joint work between Vmware Research Group, Tel Aviv University and Stanford University.