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 guarantees
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 adhere 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
Verification Reports
-
✓ OpenZeppelin Governance contracts, December 2021.
✓ SushiSwap ConstantProductPool, November 2021.
✓ SushiSwap TridentRouter, November 2021.
✓ Popsicle V3 Optimizer, November 2021.
✓ Notional Finance V2, November 2021.
✓ Celo Core Contracts Release 4, May 2021.
✓ Sushi Compound Strategy, April 2021.
✓ Balancer V2 (Issues only), April 2021.
✓ Kashi Lending Protocol, March 2021.
✓ dForce Lending Protocol, February 2021.
✓ Origin OUSD Token, February 2021.
✓ Sushi BentoBox, February 2021.
✓ 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
-
✓ To learn how to use the Certora Prover, see our Quick guide.
-
✓ In our webinars, Dr. James Wilcox presents the basics of Formal Verification and shows the Certora Prover in action, and Prof. Mooly Sagiv explains the technology underlying the Certora Prover.
-
Lesson 1 @ Celo
-
Lesson 1 @ Opyn
-
How Program Analysis with Constraint Solving Works?
-
Lesson 2: Inductive Reasoning about Smart Contracts Safety
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.
-
Synthetix
Synthetix is a derivatives liquidity protocol providing the backbone for derivatives trading in DeFi, allowing anyone, anywhere to gain on-chain exposure to a vast range of assets.
-
Origin
Origin Protocol provides a platform for building peer-to-peer marketplaces and e-commerce applications using the Ethereum blockchain. Users can buy or sell goods and services on these marketplaces, and developers can create their own applications powered by the Origin platform.
-
dForce
dForce advocates for building an integrated and interoperable open finance and monetary protocol matrix, including asset protocols (USDx, GOLDx, dToken), liquidity protocol (dForce Trade), and lending protocol (dForce Lending). Our team includes both crypto veterans and professionals from Goldman Sachs, Standard Chartered Bank, Hony Capital. dForce is backed by investors including CMBI (China Merchants Bank International), Multicoin Capital and Huobi Capital (the investment arm of Huobi Group).
-
SushiSwap
SushiSwap is a decentralized exchange used for swapping assets on Ethereum without a central authority or risk of a custodial intermediary.
-
Furucombo
Furucombo is the fastest, simplest and most comprehensive DeFi aggregator in the world that enables decentralized finance (DeFi) users to optimize and enhance their DeFi strategy.
-
Syndicate Protocol
Syndicate Protocol is a decentralized investing protocol and social network. Syndicate aims to empower more people by enabling new models for investing that are more open, free, and fair. Syndicate is backed by IDEO CoLab Ventures, Electric Capital, Delphi Ventures, CoinFund, Kleiner Perkins, and over 20 investors, angels, and founders.
-
MakerDAO Protocol Engineering Core Unit
MakerDAO enables the generation of Dai, the world's first unbiased currency and leading decentralized stablecoin. Dai is a stable, decentralized currency that does not discriminate. Any individual or business can realize the advantages of digital money.
-
Notional
Notional is a decentralized protocol that enables fixed rate lending of crypto assets on Ethereum and helps users maximize their long-term financial success.
-
Rolla Finance
Rolla Finance is a decentralized crypto options trading protocol which is making it easier than ever for users to join the future of finance. Start seamlessly buying, and selling crypto options with an intuitive, and frictionless experience with no fees, instant transactions and permissionless trading.
-
ParaSwap
ParaSwap is the go-to liquidity aggregator to beat the market price at every single swap. An API-first service with a user-friendly interface, ParaSwap has built ParaSwapPool, the first on-chain OTC DEX where professional market makers provide competitive & MEV resistant trades reaching zero-slippage and low gas costs.
-
Indexed Finance
Indexed Finance is a passive portfolio management protocol that allows users to efficiently trade baskets of self-balancing crypto assets drawn from various market sectors. Liquidity within these index products can be placed within Indexed's extensible yield-aggregator vaults, which allow funds to be permissionlessly moved across multiple lending markets simultaneously to expose holders to both the price appreciation and best-in-market interest rates of the underlying.
-
BENQI
BENQI is a leading non-custodial liquidity market protocol, built on Avalanche. The protocol enables users to effortlessly lend, borrow, and earn interest with their digital assets. Depositors providing liquidity to the protocol may earn passive income, while borrowers are able to borrow in an over-collateralized manner.
-
Orca Protocol
Orca Protocol makes governance accessible by creating tools around a DAO’s most basic primitive: people.
-
OpenZeppelin
OpenZeppelin is the premier crypto cybersecurity technology and services company, trusted by the most used DeFi and NFT projects. Founded in 2015 with the mission to protect the open economy, OpenZeppelin safeguards tens of billions of dollars in funds for leading crypto organizations including Coinbase, Ethereum Foundation, Compound, Aave, TheGraph, and many others.
Core Team
Certora Prover builds on 30 years of academic research and hundreds of academic publications which pioneered 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 the 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, and 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 received 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 is 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 received 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 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 in 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 cum laude in Computer Engineering from the Technion. He worked for two years in Apple in the CAD team.
Read more
-
Yoav Rodeh
Yoav received his PhD in formal verification from the Weizmann Institute under the supervision of Turing Award winner Amir Pnueli. He previously worked in Google, and in IBM's formal verification team. His research papers span formal verification, distributed systems, and probabilistic search questions.
Read more -
Gadi Rechlis
Gadi holds an MSc in computer science from Tel Aviv University and an Executive MBA from the Technion. Gadi brings experience in finance systems and trading strategies. In addition, Gadi is an active chess Grandmaster.
Read more -
Sameer Arora
Sameer is a Cornell University graduate who received his Bachelor's degree in Computer Science in 2020. During his degree, he focused on Logic, Systems and Compiler Design.
Read more -
Nathan Tribble
Nathan graduated from MSU Denver with a BSc in Electrical Engineering focusing on Embedded Software and Network Engineering and Computer Science focusing on Web Application Development with minors in Math and Music Theory. Nathan has spent 16 years in IT in areas ranging from Full-Stack web-development to custom Hardware/Software Solutions for Fleet Telematics and Enterprise Solutions Architecture.
Read more -
Michael George
Michael holds a Ph.D. from Cornell University, where he also served as a lecturer for 7 years. He has taught courses on everything from discrete mathematics to functional programming to operating systems. He has a broad range of interests in computer science, including formal verification, programming language design, and distributed systems.
Read more
-
Nick Armstrong
Nick holds a B.E in Computer Engineering from the University of Washington, where he focused on a combination of security and robotics with research in Human Robotic Interaction. After graduation he spent time developing computer security and encryption software before joining Certora. In his free time Nick enjoys playing soccer, competing in esports, and raising his husky, Akira.
Read more
-
Sitvanit Ruah
Sitvanit received her PhD in formal verification from the Weizmann Institute of Science under the supervision of Turing Award winner Amir Pnueli. She is the author of 15 papers and 11 patents. She previously worked in the formal verification group of IBM Research and in KayHut. Sitvanit has extensive experience in formal verification and static analysis.
Read more
-
Dan Binnun
Dan is working as a security researcher. Simultaneously, He is studying for his B.Sc. in Computer Science and Mathematics at the Bar Ilan University.
Read more -
Chandrakana Nandi
Chandrakana recently graduated with a PhD in Programming Languages and Software Engineering from University of Washington. During her PhD, she focused on developing DSLs, compilers, and program synthesizers for computational geometry. Her work has won several awards including an Adobe Fellowship and a POPL Best Paper Award. Outside of work, she enjoys long distance running with friends.
Read more
-
Eyal Hochstadt
Eyal is a B.Sc. graduate in Computer Science at the Tel Aviv University. Eyal has been a developer at the IDF, and has prior experience writing smart contracts in Ethereum. Eyal is also a professional chess player and a master's degree candidate.
Read more
-
Yoav Naftali
Yoav finished his B.Sc. in Computer Science at the Bar Ilan University. He focused mainly on deep learning and has a variety of interests in programming.
Read more
-
Aleksander Kryukov
Aleksander studied Advanced Systems Dependability as an EMJMD student. He graduated with a joint MS degree in September 2021 from the Université de Lorraine (formal reasoning) and the University of St Andrews (software engineering). He has a BS in Information Technology and Computer Engineering from Southwest State University (Kursk, Russia).
Read more
-
Ariel Grosh
Ariel is working as a security researcher. Simultaneously, He is studying for his B.Sc. in Computer Science and Mathematics at the Bar Ilan University.
Read more
-
Moran Hakkak
Experienced Administrative Assistant with 5+ years of experience working in a multinational firm. A Master of Business Administration graduate with detailed knowledge of business terminologies and standard practices.
Read more
-
Guy Dorenstein
Guy is a mathematics student at the Hebrew University. He has a variety of interests in computer science, logic and algebra.
Read more
-
Dor Geyer
Dor is working as a field security engineer. He graduated in Mathematics from Tel Aviv University and is a Master candidate at the Hebrew University in Computer Science.
Read more -
Itay Gradenwitz
Itay Gradenwits works as a security researcher, and he is about to finish his B.Sc. in Computer Science and Mathematics at the Bar Ilan University.
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
-
Jorge Navas
Jorge is an expert in theory and practice of static analysis. He loves to design and develop static analysis tools to help programmers to write more secure and bug free software. He has published papers in the top research conferences and is one of the main developers of the award-winning SeaHorn verification framework and the IKOS static analyzer. He has previously worked for NASA and Stanford Research Institute (SRI).
Read more
-
Adar Weidman
Adar is an experienced Research and Development Manager, who helped build the SAST Engine at Checkmarx. He holds a B.A. in Computer Science and an M.Sc. in Operations Research from the Technion and is a data enthusiast. He has over 30 years of experience in development for private customers, the IDF, and industry companies. Adar also holds a B.A. cum laude in Musicology from Tel Aviv University.
Read more
-
Ori Dabush
Ori works as a security researcher. He is about to finish his B.Sc. in Computer Science and Mathematics at the Bar Ilan University.
Read more
-
Shaked Winder
Shaked is about to finish his B.Sc. in Computer Science and Mathematics at the Bar Ilan University.
Read more
-
Michael Morami
Michael is working as a field security engineer. He has a deep interest in the Web3 technology and the changes it promises to bring to various industries and life domains. Michael is a physics & chemistry B.Sc. graduate from Tel Aviv University, who's also passionate about cyber security, quantum mechanics, quantum computation, condensed matter physics and more.
Read more
-
Jaroslav Bendík
Jaroslav received his Ph.D. in the areas of formal verification and constraint processing. He is the main developer of several state-of-the-art tools for analyzing infeasible Boolean and SMT constraint systems (e.g., UNIMUS or ReMUS), and his work was published at a dozen major conferences in the field. Before joining Certora, Jaroslav worked as a researcher at the National University of Singapore and at the Max Planck Institute for Software Systems.
Read more
-
Avi Adlin
Product designer with over 7 years of experience, helped building some of the most familiar interfaces in Israel. Graduated 6B collage specialized in interaction design, serves as a lecturer at Netcraft Academy for the last year. Early adopter, 3D and visual realization enthusiast.
Read more
-
Lori Blonn
Lori is a true lover of efficiency, she is passionate about excellent customer experiences, solving complex problems and coaching teams to navigate ambiguous situations. She holds a MBA with a focus in communications and has worked in both start-ups and start-ups embedded in large corporations. Her background includes defining and directing operations frameworks for corporations including Microsoft and VMware and managing production on numerous creative projects for film production companies.
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
-
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
-
Stani Kulechov
Stani Kelechov is a Finnish entrepreneur and the founder and CEO of Aave Protocol, a Leading Blockchain Startup on Decentralized Lending. Stani is also an investor and mentor of many of the leading protocols and brings his vision to shape the future and the adoption of Decentralized Finance Applications. He holds a Master in Law degree from the University of Helsinki. Stani is helping Certora with business development.
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
Careers
Security Researcher
Senior Software Engineer
Technical Project Manager
Community Manager
Security Engineer
Remote / US / Europe
We are looking for code security researchers that can understand small and tricky Solidity programs implementing financial processes. These researchers will closely work with our customers in order to find security bugs.
Job description:
Review Solidity code and find mind-blowing bugs. Communicate with customers regarding potential vulnerabilities and write technical blog posts educating the wider smart contract community. Enrich your knowledge in vulnerabilities, hacks and exploiting techniques. Become a respected white hat hacker in the community.
Relevant skills:
- Academic graduate degree in Math, Physics, or Computer Science from an excellent research university. Outstanding candidates with an undergraduate degree will also be considered.
- Background in code security especially with high-level code.
- DeFi and Fintech understanding - an advantage.
Contact Us
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!