Announcing our Series B Fundraise of $36M, Led by Jump Crypto Read more on our Blog or Daniel Jackson’s Article
Announcing our Series B Fundraise of $36M, Led by Jump Crypto Read more on our Blog or Daniel Jackson’s Article
“Certora’s technology helped to cover security on decentralized Aave Protocol, essentially finding vulnerabilities that are usually difficult to find in manual code reviews and audits. When building mission-critical software such as financial technology, Certora is a must.”
“Formal verification from Certora is the most powerful tool we have to ensure that we are building a secure, impenetrable system -- the top priority for any serious smart contract developer."
“Certora has been a crucial partner along Balancer's journey to ensure excellence in our code quality/security"
“Certora has been a critical security partner in Stakehouse Protocol’s formalization efforts. We are consistently impressed by the team’s hands-on approach and their Certora Prover tool efficacy. It reinforces the key mechanisms while giving clarity and adversarial simulation for our Multichain ETH scenarios.”
"Certora gives us so much peace of mind as we develop smart contracts at Syndicate. With formal verification running on every single commit, we can maintain a fast development velocity without decreasing security."
“Certora has unlocked TrustToken’s ability to iterate quickly while maintaining confidence in the security of our smart contracts. Our team has discovered and fixed numerous unintended bugs thanks to this powerful tool.”
"Certora has given us the ability to practically apply formal verification methods to anything we do on-chain. They have an excellent team who we've partnered with closely over the years, and the process of writing invariants with them has proven to be invaluable in writing better smart contracts."
“The Certora prover plays an important role in our overall safety strategy by providing an accessible way to quickly iterate on formal specifications and determine the correctness of bytecode. It's what we reach for when both time and safety are of the essence. Engineers can learn to use it in a few days and don't need a Ph.D. in formal methods to create good specifications. The tool recently helped us to uncover an inconsistency in an updated version of one of our oldest smart contracts, which was a surprising result. The Certora team is highly responsive and promptly addresses issues we encounter.”
.png)
.png)
Rolla Finance is a decentralized crypto options trading protocol that makes 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 is a “one-stop-shop” decentralized trading platform on Avalanche that helps users swap between two tokens.
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 makes governance accessible by creating tools around a DAO’s most basic primitive: people.
Notional is a decentralized protocol that enables fixed rate lending of crypto assets on Ethereum and helps users maximize their long-term financial success.
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.
Compound is a transparent, autonomous money market — allowing users & applications to frictionlessly earn interest or borrow Ethereum assets without relying on a counterparty.
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.
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.
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.
SushiSwap is a decentralized exchange used for swapping assets on Ethereum without a central authority or risk of a custodial intermediary.
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 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 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 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.
Bancor is a decentralized network of on-chain automated market makers (AMMs) supporting instant, low-cost trading, as well as single-sided liquidity provision and 100% impermanent loss protection for any listed token. Overseen by the Bancor DAO, the protocol’s mission is to bring DeFi mainstream by providing the simplest and safest way to trade and earn passive income in DeFi.
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 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.
✓ Benqi’s Liquid Staking Contracts, April 2022.
✓ 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.
✓ 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.
✓ 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)
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.
Software engineer with over two decades of experience in various areas. Holds a B.Sc. degree in computer science from TAU. Specializing in java internals and byte code manipulations. A bitcoin enthusiast with a deep interest in the crypto ecosystem.
Sarit holds B.Sc. in Computer Engineering from Bar-Ilan University. She previously worked as a Software Developer, with 10 years of experience in Embedded Systems and Networking.
Experienced Software Engineer, skilled in Object Oriented design, Java, holding an MSc in Computer Science from the Hebrew university in Databases and Logics.
In her last role she was Involved of developing and maintaining a search engine.
Shay is a software engineer who previously worked on distributed storage systems. He is excited about integrating formal methods to real-life software systems. Graduated Bsc in computer science from Tel-Aviv university.
Tomasz works as a security researcher. He is a Blockchain and DeFi enthusiast. Previously he was a Software Engineer in a High Frequency Trading company. He graduated in Computer Science from University of Warsaw and in Robotics from Warsaw University of Technology.
Alex holds a B. Tech degree in Electronics Engineering from IIT-BHU and an MBA from IIM Lucknow. Over the last 10 years he has worked with Amazon, L&T Group and Disney Star. He’s a Web3 and DeFi enthusiast.
Eyal is a software engineer with more than a decade of experience in cyber security.
He holds a BSc in Computer Science, Cum Laude, from The Open University.
Tal is a systems developer with 6 years of experience. She holds Bsc in mathematics & biology from Haifa university. Tal is passionate about painting, dancing & animals.
Omer is a senior software engineer working as a backend developer. Omer received his M.Sc. in computer science at Tel-Aviv university.
He has experience in embedded systems and cyber security.
Gadi holds MSc in Computer Science from the Hebrew University. He previously worked at IBM and Intel with 20 years of experience in formal verification application of microprocessors, detecting dozens of subtle corner-case bugs in numerous protocols and logic design of top-end complex systems, and leading a team of FV experts.
Daniel is a security researcher, with over 7 years of experience as a security researcher and engineer in the fields of network and web vulnerability exploitation.
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.
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.
Armen graduated with a BSc in Mathematics from UC Irvine. He is interested in smart contract security and permissionless systems.
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.
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.
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.
Yuval has a 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.
Rahav holds a B.Sc. degree in Computer Sciences from the Hebrew University and an MBA from the Kellogg – Recanati program. For the last 5 years, he has worked as a full-stack engineer for Solarwinds. Before that, he worked for 14 years for the Nokia Research Center, both in Finland and the US. He also worked for the SanDisk Innovation Group and Red Bend as a Director of Standards.
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.
Frontend software engineer and Computer Science and Cognitive Science student in the Hebrew University of Jerusalem.
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.
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!
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.
Roi is studying for his B.SC in computer engineering and mathematics at Bar Ilan University.
Netanel is a theoretical mathematician with an active interest in Blockchain technology. He received his PhD from MIT in 2016. Before that, he served as a researcher in the IDF working at the intersection of data science, algorithm development, and vulnerability research.
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.
DeFi enthusiast with extensive experience in web3 development and trading strategies. Yura holds a B.Sc. in Computer Science from the Hebrew University.
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.
Nathan is a Web Developer with 3 years of experience.
Graduated from the Technion external studies.
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 an 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.
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 at several top conferences in the field.
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.
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 about making formal verification real.
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.
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.
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.
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.
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.
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.
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.
Yoav received his PhD in formal verification from the Weizmann Institute under the supervision of Turing Award winner Amir Pnueli. He previously worked at Google, and IBM’s formal verification teams. His research papers span formal verification, distributed systems, and probabilistic search questions.
Guy is a mathematics student at the Hebrew University. He has a variety of interests in computer science, logic and algebra.
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.
Shaked is about to finish his B.Sc. in Computer Science and Mathematics at Bar Ilan University.
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.
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).
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.
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.
Uri is a Software Engineer who graduated cum laude in Computer Engineering from the Technion. He worked for two years at Apple in the CAD team.
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.
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.
Blockchain enthusiast with a background in Formal Verification. She is also an experienced software engineer who 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.
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 that 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.
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.
Ori works as a security researcher. He is about to finish his B.Sc. in Computer Science and Mathematics at the Bar Ilan University.
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).
Ariel is working as a Software Engineer. Simultaneously, He is studying for his B.Sc. in Computer Science and Mathematics at Bar Ilan University.
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.
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.
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.
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.
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.
Product designer with over 7 years of experience, helped build some of Israel’s most familiar interfaces. Graduated 6B college specializing in interaction design, and has served as a lecturer at Netcraft Academy for the last year. Early adopter, 3D and visual realization enthusiast.
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.
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.
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.
Simon is a seasoned technology executive and consultant with over 20 years of 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.
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.
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.
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.
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.
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.
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).
Remote / Europe
Requirements
MUST
ADVANTAGE
SOFT SKILLS
Responsibilities
This is exactly the intended use case of 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.
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.
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.
Definitely, and we will assist you and review your rules for free.
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.
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.
The Certora prover currently analyzes EVM bytecode combining two computer science techniques: abstract interpretation and constraint solving. These are well understood academic fields.
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!
