Certora Community Update - July 2022
Headlines from June 2022
Two AAVE formal verification community grant rounds have been completed! Congratulations to the winners who earned thousands of USD. The two projects chosen by the community were StarkNet's bridge and LidoFinance’s AstETH.
More rounds are coming in the next few months. Register here and help improve DeFi security and win rewards!MakerDAO’s Protocol Engineering Core Unit has discovered that the fundamental equation of Multi-Collateral DAI does not hold, despite the equation being known since 2018 and thought to be mathematically provable
A new previously unknown Solidity compiler optimizer bug in versions 0.8.13 and 0.8.14 that causes silent discard of important memory operations has been found by John Toman, our VP of R&D
We released a new version of the Certora Prover, which includes a new look for the results page.
The Certora Prover prevented critical bugs in Compound Finance’s Version 3 (Comet). Read the verification report.
We created a new dashboard for the AAVE community where we display properties of ERC20 tokens that are candidates for listing in the AAVE platform. Testing the token code against our specification provides knowledge and richer details to the community to make a better-informed decision about the asset.
Articles
Certora brings a new, game-changing tech from the emerging verification sector to smart contract security. What is unique about our technology, and how does it work? MIT Professor Daniel Jackson explains.
Watch how formal methods can be used to improve the safety of DeFi projects in this talk by our CEO, Professor Mooly Sagiv, at TrustX.
Formal verification's ability to find critical bugs depends on the quality of the specification. Learn what are some common errors in specifications and how to avoid them.
When checking Compound’s Comet, we applied modularity by breaking the code into two pieces and checking each piece separately. Read more on how to use formal verification on complex code such as Comet.
Watch a #Certora_seminar with Dimitar Bounov from Consensys speaking about Scribble, a language for describing bad patterns in smart contracts. Dimitar is the architect of Scribble and its implementation and has a Ph.D. from UCSD.
Events
Certora’s security researcher Yura Sherman, together with senior researcher Jaroslav Bendik, and community advocate Uri Kirstein, presented a workshop at ETHPrague about previous bugs in ERC20 tokens and which properties of tokens do they break.
We sponsored and attended PLDI, which is a premier forum in the field of programming languages and programming systems research, covering the areas of design, implementation, theory, applications, and performance.
Stay tuned for
“Formal Verification for fun and Profit“ - Certora is holding a workshop for beginners and experts alike at ETHCC. Three days of lectures and hands-on exercises that will teach you everything you need from the ground up, or will elevate your existing skills.
Register here
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