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
-
✓ Benqi’s Liquid Staking Contracts.
✓ 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
-
Auditing and Formal Verification: Better together
View PDF -
Understanding the Workflow of the Certora Prover
-
ETHDENVER – MOVE FAST AND BREAK NOTHING MICHAEL GEORGE
-
Workshop: Aave Community Day 1 4/27/22
-
Workshop: Aave Community Day 2 4/28/22
-
Workshop: Aave Community Day 3 4/29/22
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
-
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.
-
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.
-
TRADER JOE
Trader Joe is a “one-stop-shop” decentralized trading platform on Avalanche that helps users swap between two tokens.
-
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.
-
ORCA PROTOCOL
Orca Protocol makes governance accessible by creating tools around a DAO’s most basic primitive: people.
-
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.
-
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.
-
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.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.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.
-
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.
-
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.
-
Silo
Silo is a risk-isolating lending protocol that implements permissionless lending markets where any token can borrow another. Silo is secure by design – each lending market supports two assets only, the bridge asset and a unique token asset. This design concentrates liquidity in single pools and allows for efficiency.
-
Morpho
Morpho is a Peer-to-Peer (P2P) layer on top of lending pools like Compound or Aave. Rates are seamlessly improved for both suppliers and borrowers whilst preserving the same liquidity and market risk guarantees.
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.
-
Naftali Goldstein
A software engineer with almost a decade of experience in embedded systems and communication protocols. Naftali holds a B.Sc. in Mathematics and an M.Sc. in Computer Science, both from the Hebrew University.
Read more -
Amit Sassi
Finance enthusiast, passionate about startups, SAAS business model, financial modeling, and corporate finance.
As a CPA, Amit has vast experience in the financial area. He holds a Master’s degree in accounting and finance from Tel-Aviv University, as well as a Bachelor of Arts degree in Accounting and Business Administration from the Hebrew University of Jerusalem.
A constant learner, tech savvy with a hands-on and lead-by-example approach.Read more
-
Armen Ter-Avetisyan
Armen graduated with a BSc in Mathematics from UC Irvine. He is interested in smart contract security and permissionless systems.
Read more -
Thomas Adams
Thomas is a data scientist, educator, and enthusiastic generalist who brings his love of grammar, formal logic, and communication to security engineering. He earned a Bachelor’s Degree in Chemistry from Carleton College before teaching sciences, languages, and music at the secondary level. As a consulting data scientist at Fred Hutchinson Cancer Research Center, he helped disease researchers incorporate machine learning algorithms and other data science techniques into their work. He loves analyzing how systems function and how humans learn and interact with them. Thomas is excited to apply his broad background to the formal verification space at Certora.
Read more -
Alexander Bakst
Dr. Alexander Bakst is interested in developing tools that enable programmers to build trustworthy systems. He has previously worked in an industrial setting on both compiler and operating system development and has experience as a researcher and practitioner of formal methods for software engineering. Dr. Bakst holds a PhD from UC San Diego.
Read more
-
Benjamin Greenwald
Ben studied programming languages, compilers, and computer architecture at UC Berkeley and MIT. He has over 15 years of experience building commercial program analysis solutions for application security and correctness, working for companies such as Ounce Labs and Veracode.
Read more
-
Yuval Bendor
Yuval has deep interest in programming language design, compilers and optimization. He is passionate about systems programming, as well as programming for constrained architectures. He holds a B.Sc in computer science from the Hebrew University of Jerusalem and has developed verification and system simulation tools at Cadence Design Systems.
Read more -
Rahav Yairi
Rahav holds B.Sc. degree in Computer Sciences from the Hebrew University and an MBA from the Kellogg – Recanati program. For the last 5 years he worked as a full stack engineer for Solarwinds. Before that he worked 14 years for the Nokia Research Center both in Finland and in the US. Also worked for the SanDisk Innovation Group and for Red Bend as a Director of Standards.
Read more
-
Gavriel Elizedek
Gabriel is a software engineer with vast experience that extends over decades, from various corners of the Israeli High-Tech industry, starting at the IDF. Studied at Tel-Aviv University for B.A. in Mathematics and Philosophy.
Read more
-
Noa Babliki
Frontend software engineer and Computer Science and Cognitive Science student in the Hebrew University of Jerusalem.
Read more -
JEFF STEGER
Jeff holds a bachelor’s in physics, a bachelor’s in computer science (both from Binghamton University), and a Master’s in Electrical Engineering (from Syracuse University). He has worked in the defense industry, the financial industry, and the cybersecurity industry designing and developing time-sensitive server-side applications (largely in C++). He is married with two daughters and has been living in Florida for the past 10 years and loves it. In his spare time, he collects comic books and tries to wrap his mind around decentralized finance.
Read more -
Shahar Matsa
Shahar holds a B.Sc in computer science (magna cum laude) from the Open University of Israel, which he started alongside his studies in an accelerated gifted class in high school (From which he graduated with Bagrut with summa cum laude), and finished prior to serving almost 3 years in the IDF as a programmer in an R&D unit of the IAF.
He has a strong passion for computers and automation, for algorithms and math, and for everything that makes him think and use logic!Read more -
Alex Stoliar
Alex is a Blockchain and Defi enthusiast. In his previous roles he led the development of a blockchain project at JP Morgan and worked as a Software Engineer at COTI. He is a Computer Science B.Sc graduate from Ben Gurion University.
Read more
-
Roi Even Haim
Roi is studying for his B.SC in computer engineering and mathematics at Bar Ilan University.
Read more
-
Netanel Rubin-Blaier
Netanel is a theoretical mathematician with active interest in Blockchain technology. He received his PhD from MIT in 2016. Before that, he served as a researcher in the IDF working in the intersection of data science, algorithm development, and vulnerability research.
Read more
-
Roy Perry
Roy is a M.Sc in physics from Ben-Gurion university. He has 6 years of programming experience mostly in the field of computational physics. He also has an interest in mathematics and enjoys solving cryptic crossword puzzles.
Read more
-
Yura Sherman
DeFi enthusiast with extensive experience in web3 development and trading strategies.Yura holds a B.Sc. in Computer Science from the Hebrew University.
Read more
-
Gad Elbaz
Gad graduated from BGU Be’er Sheva with a BSc in Computer Science. Gad has spent 10 years in IT focusing on Cyber-Security in areas ranging from hacking Network- infrastructure & endpoint computers to developing anti-fraud Web Solutions.
Read more
-
Nathan Gur-Arie
Nathan is a Web Developer with 3 years of experience.
Graduated from the Technion external studies.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
-
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 -
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 -
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
-
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
-
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
-
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 -
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
-
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
-
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
-
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
-
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 -
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
-
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
-
SHAKED WINDER
Shaked is about to finish his B.Sc. in Computer Science and Mathematics at the Bar Ilan University.
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
-
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
-
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
-
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 -
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
-
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
-
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 -
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
-
YUVAL ZALMENSON
Self-motivated hands-on software engineering leader with over 15 years of experience in the domains of network security, storage systems and L1 blockchain protocols. Passionate about solving hard problems and learning what tickles people. I have an M.Sc in Computer Science from the Interdisciplinary Center Herzliya and B.Sc in Mathematics and Computer Science from the Technion.
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
-
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
-
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
-
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
-
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 -
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
-
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
-
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 -
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
Advisory Board
-
Mudit Gupta
Mudit is the Chief Information Security Officer at Polygon. He has been in the blockchain space for 8+ years and has led research & development at projects like SushiSwap and Polymath. Mudit comes from a traditional cyber security background and bridges the gap between traditional security and blockchain security.
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
-
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
-
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
-
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
-
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
-
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
-
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
-
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
-
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
Careers
Security Engineer
Community Manager
Technical Project Manager
Senior Software Engineer
Security Researcher
Remote / US / Europe
Certora is developing cutting edge tools for guaranteeing software correctness.
We are looking for security engineers that will apply formal verification technologies to business-critical financial applications handling billions of dollars. These financial applications are lucrative targets for hackers.
Our engineers will work closely with our customers to find security bugs and prove their absence.
JOB DESCRIPTION:
Comprehend complex financial systems written in Solidity code. Mathematically formalize interesting properties of DeFi and deploy Certora’s tool for automatic exact formal verification, analyze outputs of the tool to identify high severity vulnerabilities. Write public reports describing the verified properties.
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.
- Previous experience SW development.
- Background in code security especially with high-level code (an advantage).
- DeFi and Fintech understanding (an advantage).
- Formal verification background (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!
