About Certora
We are the only team which provides
Prover technology
for checking security rules
with the following features:
-
Minimal false alarms
Reported errors are real
-
Formal correctness guarantess
For proven rules, no missed alarms
-
Fully Automatic
No need for human intervention
-
Agile
Supports arbitrary programs and integrates into CI/CD pipeline
Certora for Business
Static Asset Scanner: A monitor layer for smart contracts providing up to the minute security of the bytecode.
Certora for Developers
Quality Development Environment: A CD/CI platform for smart contract development.
Technology
Certora provides security analysis tools for Smart Contracts. Certora has unique technology called Certora Prover capable of checking at compile-time that all executions of a Smart Contract fulfill a set of security rules.
Certora Prover technology is available as a tool that complements existing compilers and debuggers of Smart Contracts. It checks that the contracts adheres to the interface requirements of other contracts. Certora’s blockchain independent and language-agnostic Prover technology precisely identifies bugs in Smart Contracts and proves their absence.
Contact Us
Blog
-
✓ Our first post explains Why testing is not enough for million-dollar code.
-
✓ In our second post, we demonstrate how Certora's Prover can uncover tricky reentrancy bugs, as we discovered in leading DeFi platform Synthetix.
-
✓ Our third post describes a memory corruption vulnerability in code generated by the Solidity compiler.
-
✓ Certora Bug Disclosure: Lost Signer Fees in the TBTC system.
-
✓ A new bug in the Solidity compiler is causing corruption of storage.
-
✓ Another new bug in the Solidity compiler may lead to non-deterministic behavior.
-
✓ Build secure smart contract upgradability mechanisms with the Certora Prover.
Verification Reports
-
✓ Opyn Gamma Protocol, December 2020.
✓ Synthetix Multi-Collateral Loans, December 2020.
✓ Aave Protocol V2, December 2020.
✓ Keep's Fully-backed bonding contract, November 2020.
✓ Compound's Open-Oracle with Uniswap Anchor, August 2020.
✓ Celo Governance Protocol, May 2020.
✓ Orchid's Smart Contracts, December 2019.
✓ Compound's MoneyMarket v2 formal verification report, August 2019.
Education
Webinars & User Guides
-
Lesson 1 @ Celo
-
Lesson 1 @ Opyn
-
✓ Dr. James Wilcox presents the basics of Formal Verification and shows the Certora Prover in action.
-
✓ To learn how to use the Certora Prover, see our Quick guide.
Academic Papers
-
✓ Our SBC paper describes how generic rules can be used to find bugs.
-
✓ Our OOPSLA'2020 paper presents the most precise way for proving a code is immune to reentrancy-style attacks. (Video)
Customers
-
Coinbase
Coinbase is a leading digital currency exchange based in San Francisco, providing professional and consumer grade trading products allowing users to buy, sell, send, and receive most major digital assets.
-
Compound Finance
Compound is a transparent, autonomous money market — allowing users & applications to frictionlessly earn interest or borrow Ethereum assets without relying on a counterparty.
-
Celo
Celo is an open platform that makes financial tools accessible to anyone with a mobile phone.
-
Orchid
Orchid is a decentralized virtual private network (VPN), allowing users to buy bandwidth from a global pool of service providers.
-
Aave
Aave Protocol is a decentralized, open-source, and non-custodial money market protocol. Depositors can deposit assets into the protocol and earn interest on their deposits without relying on middlemen
-
Opyn
Opyn is a product and open protocol on Ethereum that allows users to buy, sell, and create options on any ERC20. DeFi enthusiasts and projects alike rely on Opyn’s smart contracts and interface to hedge themselves against DeFi risks and take positions on different cryptocurrencies.
-
tBTC
tBTC is an open-source project supported by groups including Keep, Summa and the Cross-Chain Group. tBTC is a fully Bitcoin-backed ERC-20 token pegged to the price of Bitcoin. It facilitates Bitcoin holders acting on blockchains and accessing the decentralized finance ecosystem.
-
Balancer
Balancer is a protocol for programmable liquidity. It allows for the creation of self-balancing liquidity pools with flexible parameters. A pool can have 2 or more tokens and each token can have different weights. Balancer also allows for smart pools which have evolving parameters: think of a surge pricing liquidity pool that increases the trading fees in times of high volatility/demand for liquidity.
Core Team
Certora Prover 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.
-
Nurit Dor
Nurit holds a PhD from Tel Aviv University in Static Code Analysis. She is an author of 13 academic papers and 35 patents. She was a CSO at Panaya, a static-analysis company acquired by Infosys and a research manager at KayHut. Nurit has extensive experience in static and dynamic analysis of low-level bytecode. Hands-on experience in transferring ideas from research to robust products.
Read more
-
Anastasia Fedotov
Anastasia is a software engineer, working as a full-stack developer on Certora's SaaS product. Anastasia got her B.Sc. in Computer Science and Economics at Tel-Aviv University.
Read more -
Shelly Grossman
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.
Read more
-
Mooly Sagiv
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. He has more than 200 academic publications with Google H-index 55.
Read more
-
James Wilcox
Dr. James Wilcox recieved his PhD. in June 2019 from the University of Washington. Dr. Wilcox is the architect of a system called Verdi for formally verifying distributed systems. He is an author of 15 academic papers. He is enthusiastic to make formal verification real.
Read more
-
Thomas Bernardi
Thomas recently received his Bachelor's Degree in Computer Science from the University of Washington. During his degree he focused on Programming Languages and Formal Methods and he is glad to have found a place where he can directly apply those skills. In his free time he enjoys long distance running and volunteering at his local food bank.
Read more
-
Lior Oppenheim
Lior is a security researcher with over 6 years of experience in the vulnerability and exploitation fields. In his spare time, Lior is also an MSc. student for physics at the Weizmann Institute.
Read more
-
Alexander Nutz
Alexander likes logic. He did his PhD research all over the areas of program verification, static analysis and SMT. He published several research papers and is one of the main developers of the award-winning program verification tools of the Ultimate framework (e.g. Ultimate Automizer, Kojak, TreeAutomizer, Unihorn Automizer). He also worked on the interpolating SMT-solver SMTInterpol.
Read more
-
Or Pistiner
Or holds a BSc in Computer Science, Cum Laude, from Tel Aviv University. He received his MSc in Computer Science from Tel Aviv University in 2019. His research focuses on automated synthesis of reactive systems from specifications, specifically, making this technology useful for software engineers. He is one of the developers of Spectra, a specification language and tools for reactive synthesis. He has co-authored several research papers that tackle the challenge of enriching the specification language while still maintaining synthesis scalable.
Read more -
John Toman
Dr. John Toman received his PhD in 2019 from the University of Washington. Dr. Toman's research focuses on bringing the power of automated verification to real world, industrial settings. His award-winning, impact focused research has been published in several top conferences in the field.
Read more -
Uri Kirstein
Uri is a Software Engineer graduated in Computer Engineering from the Technion. He worked for two years in Apple in the CAD team.
Read more
Advisory Board
-
Prof. Alex Aiken
Alex is the Alcatel-Lucent Professor of Computer Science at Stanford. Alex received his Bachelors degree in Computer Science and Music from Bowling Green State University in 1983 and his Ph.D. from Cornell University in 1988. Alex was a Research Staff Member at the IBM Almaden Research Center (1988-1993) and a Professor in the EECS department at UC Berkeley (1993-2003) before joining the Stanford faculty in 2003. His research interest is in areas related to programming languages. He is an ACM Fellow, a recipient of Phi Beta Kappa's Teaching Award, and a former chair of the Stanford Computer Science Department (2014-18).
Read more
-
Prof. Jeff Flowers
Jeff Flowers interests in computers began with the realization of the power of open and private communication in the early 90s with the release of PGP. From this initial spark demonstrating how applied cryptography could empower the individual to then seeing these techniques used to create novel global communication networks, he has continued his exploration of these powerful tools. He was Director of Curriculum and Instruction at Blockchain University and continues to lecture at DLT Education on the emerging field of Blockchains. At Certora Jeff provides a lens crafted from the numerous Blockchain and DLT based projects he is associated with, as well as being an active member of multiple technology focused communities around Silicon Valley. When he is not working on these endeavors, Jeff is a tenured Professor at the College of San Mateo's Math Sciences Division teaching Chemistry. His doctoral work, at San Francisco State University, focused on the use of neural networks and gamification protocols towards the optimization of educational pathways.
Read more
-
Aviva Gatt
Aviva has 25+ years industry experience in People leadership of global high growth companies- supporting & growing early stage start-up environments. She established & staffed global subsidiaries, helped build global executive teams and the development of innovative, highly professional and close-knit company cultures. She led 6 successful HR M&A integrations. Aviva has a BA in Social Work from the Hebrew U and an MBA in Human Resources & Management from NY Polytechnic.
Read more
-
Dr. Yona Hollander
Yona is a seasoned industry expert and entrepreneur, he has over 20 years of management and technology experience in the cyber security space. Yona was a co-founder of Fortsacle in the area of User Behavioral Analysis (UBA) which was acquired by RSA at 2018. Prior to founding Fortscale, he founded and managed Cyber Security, a boutique technology consulting firm. Yona also was a founder and served as VP of Security Research at Entercept, which was acquired by McAfee in 2003 for $120M. Yona then continued as VP of Security Research at McAfee HQ in Santa Clara. Before that, he worked as VP of Business Development at Netect, a pioneer in vulnerability assessment technology, which was acquired by BindView in 1999. Yona holds a PhD. in Computer Science from the Israel Institute of Technology (Technicon).
Read more
-
Prof. Neil Immerman
Immerman is a renowned computer scientist studying logic in computer science and descriptive complexity. He received B.S. and M.S. degrees from Yale University in 1974 and his Ph.D. from Cornell University in 1980. His book Descriptive Complexity appeared in 1999. He received a Göedel Prize for solving a 20 year open problem in computer science theory. Immerman is an ACM Fellow and a Guggenheim Fellow.
Read more
-
Prof. Daniel Jackson
Daniel Jackson is a Professor of Computer Science at MIT, a MacVicar teaching fellow, and an Associate Director of the Computer Science and Artificial Intelligence Laboratory. His research has focused primarily on software modeling and design. He was the creator of the Alloy modeling language, and author of Software Abstractions: Logic, Language, and Analysis (MIT Press; second ed. 2012). His current research projects include development of new paradigms for end-user programming, a safety interlock for self-driving cars, and a new theory of software design that connects user experience to essential conceptual structures. He was a recipient of the 2016 ACM SIGSOFT Impact Award, the 2017 ACM SIGSOFT Outstanding Research Award, and is an ACM Fellow. Jackson is also a photographer; his most recent project is Portraits of Resilience.
Read more
-
Uri Kolodny
Uri is a co-founder and CEO at StarkWare, and a member of its Board of Directors. He has a BSc (Magna cum Laude) in CS from the Hebrew University, and an MBA from MIT Sloan. Uri is a serial entrepreneur, who has co-founded several technology companies, among them OmniGuide (an MIT spinoff developing optical fibers for endoscopic surgery), and Mondria (developer of tools for visualization of big data). Previously, Uri also served as an EIR with two Israeli VC firms, and as an analyst at McKinsey.
Read more
-
Avihu Levy
Avihu has a BSc (Summa cum Laude) in EE and Physics from the Technion. He has 8 years of experience in security research of network protocols and mobile devices. Avihu is a blockchain enthusiast, and has worked on several projects in the field, including co-founding a cryptocurrencies algo-trading startup. Avihu is the head of product at StarkWare.
Read more
-
Simon Morris
Simon is seasoned technology executive and consultant with over 20 years experience in Silicon Valley and a deep knowledge of decentralized technologies and the peer-to-peer space. He worked for almost 10 years at BitTorrent Inc in many roles including Chief Strategy Officer and General Manager. He led the design of what became known as BitTorrent's BTT token technology and played a key role in the subsequent sale of the company. He holds an MBA from Stanford University Graduate School of Business and MPhil and BA/MA degrees in Politics and Economics from Cambridge University.
Read more
-
Moti Rafalin
Software executive and entrepreneur with over 20 years of experience in the enterprize software market with a focus on infrastructure and security. Co-founder and CEO at vFunction, currently in stealth mode, and of WatchDox which was acquired by BlackBerry. Before co-founding WatchDox, was the General Manager of the Application Management Business at EMC. A graduate of the Technion, Israel Institute of Technology (Summa cum laude), and holds an MBA from the Harvard Business School.
Read more
-
Prof. Noam Rinetzky
Noam Rinetzkey is an expert in formal verification, programming languages, concurrent and distributed systems. He developed core correctness requirements for concurrency control. He received a PhD in computer science from Tel Aviv University. Noam is a recipient of the prestigious IBM scholarship for his PhD studies and Royal Academy of Engineering/EPSRC Research for postdoctoral studies.
Read more
FAQ
-
Can we use the Certora Prover in our CI pipeline? This is exactly the intended use case of the Certora prover!
-
What can be tested or proven using the Certora Prover? The Certora Prover provides complete path coverage for a set of safety rules provided by the user. For example, a rule might check that only a bounded number of tokens can be minted in an ERC20 contract. The prover either guarantees that a rule holds on all paths and all inputs or produces a test input that demonstrates a violation of the rule.
-
What cannot be tested using the Certora Prover? The problem addressed by the Certora Prover is known to be undecidable. This means that there will always be pathological programs and rules for which the Certora prover will time out without a definitive answer. Our experience so far is that realistic customer’s programs are not pathological and can be successfully analyzed by the Prover. The Certora team is actively working to reduce the number of timeouts when analyzing smart contracts of customers.
-
How does formal verification differ from a traditional security audit? A traditional security audit usually involves a manual, holistic review of an entire system. Formal verification, on the other hand, produces a proof that a piece of software satisfies a specification. The Certora team is available for formal verification projects to write specifications and verify the code against these specifications. Often, verification projects find bugs in the code, and these bugs can be fixed during the course of the project, with the fixes proved correct. The team also produces a report describing the properties verified and bugs discovered. At the moment, we only analyze and review Ethereum bytecode.
-
Can we program our own rules into the prover into the future? Definitely, and we will assist you and review your rules for free.
-
What are the inputs to the Certora Prover? The Certora Prover takes as input the smart contract (either as EVM bytecode or Solidity source code) and a set of rules, written in Certora’s specification language. The Prover then automatically determines whether or not the contract satisfies all the rules. Just as good testing sometimes requires code refactoring, verification occasionally requires changes to the code. For example, because the verification happens via the public API to the contract, some state pieces may need to have getters added so that they are accessible.
-
How do I know that the written rules are correct? When the Certora Prover provides a test input that violates the rule, the user can check if this violation is due to a bug in the code or the verification rule. We also suggest performing a sanity check on the rules, e.g., by mutating the contract by adding an artificial bug and checking if any rule is violated. If no violations were found, the specification is missing a rule. The Certora Prover also automatically generates test cases for showing that a point in the program is reachable.
-
What is the technology behind the Certora Prover? The Certora prover currently analyzes EVM bytecode combining two computer science techniques: abstract interpretation and constraint solving. These are well understood academic fields.
-
How does the Certora Prover differ from existing tools in the market? Unlike symbolic execution tools which select specific paths and a fixed set of bad patterns, such as MythX and Slither, the Certora Prover provides complete coverage for a user provided set of rules. Interactive theorem provers such as Coq and K can be used for interactively showing that a specific contract is correct. SMTChecker by the Solidity team and Verisol by Microsoft Research are similar to the Certora Prover in many respects but target Solidity sources with per program user assistance. This makes the tools hard to integrate into the CI pipeline --- the value of the verification is that it allows to move fast and break nothing!