Certora Community Update - August 2022
Headlines from July 2022
Certora will release a new and improved way of configuring a verification run via our VSCode extension in August. Here is a sneak peek
Certora is happy to collaborate with The Secureum for the second time, now in a joint effort with the AAVE formal verification community grant. Secureum participants will be learning how to use the Certora Prover, and apply their knowledge to find bugs in the smart contracts chosen by the AAVE community.
We are happy to secure the V3 of Compound (Comet) to be soon launched. See our verification report and the several critical issues we have prevented.
An AAVE formal verification community grant project has concluded - verifying Lido Finance’s AstETH. A total of 19.5K$ have been granted in awards. During this project, the community contributed a total of 25 specification rules, some of which will be included in our official specification of the contract.
We are happy to announce a new partnership with Morpho, developing an on-chain Peer-to-Peer layer on top of lending pools that increases capital efficiency.
As part of our AAVE continuous verification proposal, we have verified three governance cross-chain bridges L2 executors: Polygon, Optimism, and Arbitrum. Additionally, we inspected Avalanche's sAVAX oracle adapter, and found one low-priority issue which GDBLabs quickly fixed.
Articles
Formal Verification for Fun and Profit
Missed our three day workshop at EthCC? You can now view its entirety. Aimed at beginners, it will teach you how to use the Certora Prover to find bugs. Our best speakers' talks will elevate your skills even if you are familiar with the Certora Prover.What is the technology behind the Certora Prover? How is it different than fuzzing? PhD Michael George, our Head of Product, explains:
Move Fast and Break Nothing
Watch our CEO, PhD Mooly Sagiv, at EthCC explain how the Certora Prover allows developers to change their code frequently during development while ensuring its security.Smart Contract Exploits
Our security engineer Yura Sherman spoke about DeFi vulnerabilities in the Israel Web3 Dev Meetup. Yura explains why smart contracts are vulnerable, and presents common types of attacks with historical examples, in Hebrew.
Events
Certora had a significant presence at EthCC 2022. We held a three-day workshop, Formal Verification for Fun and Profit, that taught the participants how to use our tool. Our CEO Mooly Sagiv gave a talk, Move Fast and Break Nothing. Recordings of both can be found above. It was fun meeting all of you in person in Paris!
Certora had a booth at ETHBarcelona! We were excited to meet you all and give away some of our magical swag.
Stay tuned for
Formal Verification for Fun and Profit
A three-day workshop at Stanford. Day 1 & 2: A beginner workshop on the basics of the Certora Prover. Day 3: An advanced workshop focused on formal verification of AAVE. Participants will work on AAVE community projects together, and they can earn up to 10k in grants. You’ll receive a key to access the Certora Prover for 3 months.
Stanford, August 29-31, 2022, during SBC’22 and following DeFi Security Summit. Register here.
DeFi Security Summit
Join the first annual event dedicated to all things security related in DeFi. Some of the best speakers in the field will discuss a wide range of topics, including DeFi Protocols, Auditing, Bridges, Security Tools, White Hat Hacking, Insurance, Exploits, and more. Paul & Mildred Berg Hall, Stanford, August 27-28. The event is free, but space is limited - reserve your place!
Defi Security 101
Are you fascinated by code correctness? Want to learn more about DeFi security? Attend DeFi Security 101, a one-day crash course on DeFi security at Stanford, on August 26th, right before the Defi Security Summit.
Formal Reasoning about Financial Systems Workshop
This one-day academic workshop brings together researchers developing tools for reasoning about financial systems and smart contracts. The workshop includes a wide array of world experts in all fields of Formal methods that will discuss the theory behind static program analyzers, fuzzers, formal verification tools, Satisfiability Modulo Theorem checkers, and more. The workshop follows SBC’22 on September 1st, Gates 403, Stanford.
Federated Logic Conference 2022
We sponsor the mentoring workshop at FLoC 2022, the 8th Federated Logic Conference, held at the Technion, Haifa, Israel, between August 1st - August 17th.Formal Verification of Ethereum Smart Contracts: SMT-Based Approaches and Challenges
Our senior researcher, PhD Jaroslav Bendik, is presenting at The Workshop on Democratizing Software Verification on August 11th, Haifa, Israel.Verifying smart contracts: SMT real life challenges and solutions
Our senior researcher, PhD Yoav Rodeh, is presenting at ICALP on August 17th, in Haifa, Israel.ETHWarsaw
We are proud to sponsor ETHWarsaw, the biggest Web3 hackathon & conference in the CEE region. Certora will hold a short workshop, give a talk, and participate in a security panel, details TBD. Tickets are now on sale.
We are hiring!
Technical Roles: If you are a geek of logic, compilers, programming language design, financial math, or developer tools — we want to hear from you. Certora is looking for full-time Developers to join the Compilers, Web, DevOps, and Security teams and make formal verification a standard in the industry in Smart contracts and beyond. We want to expand our tools to other blockchains, including Web Assembly based chains such as Polkadot.
Non-Technical Roles: Certora is looking for business, community, and PR experts to make formal methods a standard practice in DeFi and beyond.
Interested? Check out our careers page