Certora Community Update - November 2022

Headlines from Q4 2022

• Check out our white paper outlining the technology that sets us above the rest. You’ll gain an understanding of our Certora Prove, including its power and current limitations.

  

• We won the renewal proposal vote for continuous formal verification of the AAVE protocol. We thank the AAVE stakeholders for their support. We are excited to continue improving the security of AAVE by formally verifying new contracts and fostering the AAVE security community together with the Secureum.

• We joined forces with Balancer, launching the Balancer Certora Security Accelerator, which helps projects building on Balancer increase their code security. The Security Accelerator will grant access to Certora’s formal verification Prover and provide code reviews. This partnership will strengthen the soundness of the code base and streamline the go-to-market process for upcoming projects. Full Details and registration here: full announcement.
  

  

• Morpho completed the first part of their formal verification work with our Certora prover - the $MORPHO token.

  

• SaaS customer pStake Finance formally verified their most critical staking contract with Certora. pStake’s product allows staking PoS assets while earning DeFi yields.

  

• Blockswap Labs collaborated with Certora to conduct a joint formal verification of its Stakehouse main net protocol codebase. We are excited to formally verify the correctness of a complex, cutting-edge technology like Stakehouse’s multi-chain, permissionless, non-custodial programmable staking.

• Certora SaaS customer Silo Finance has deployed a fully decentralized lending protocol on Ethereum. Check out their self-published verification report where they found and fixed 2 high severity bugs (and more)

Read

• Are you using formal verification early in the code development process? Our new article explains why you should - Shift Left: Formal Verification First, Not Last!

Watch

• How can you write specifications that will uncover bugs? What are the different types of properties that one can specify? Nurit Dor, our VP of Product, explained at the DeFi Security Summit:

• Formal verification can be a huge boon to smart contract security as it checks all possible execution paths. Unfortunately, even verified code can be faulty if the formal specification contains mistakes. "Bad" proofs can lead to false confidence in the code and premature deployment. Watch Uri Kirstein, Certora’s Developer Relations and a developer, discuss different types of "bad" proofs and how to avoid them in his talk at Devcon.
  

• Formal verification is a technique for detecting bugs and mathematically proving their absence. By comparing the existing behavior of the program to its desired behavior, code security is drastically increased. However, most tools do not scale to handle realistic programs. Our CEO Mooly Sagiv explained how the Certora Prover successfully verifies programs with 10,000 lines of Solidity code at ETHBogota.
  

• Listen to a lightning talk about the Certora Prover at the DeFi Security Summit by Michael George, Certora’s Head of Product:

• How can you find bugs in smart contracts with formal verification? Our security engineer Yura Sherman explained in ETH Bogota:

• Certora held a two-day workshop at Stanford, following the DeFi Security Summit that explains from scratch how to use our tool to find bugs in smart contracts. You can watch the recordings of both days:
  

• Smart contract security audits have become a de facto requirement for Ethereum applications. However, there continue to be multi-million dollar hacks every week highlighting significant challenges with audits such as questionable quality, arguable effectiveness, unreasonable expectations, high cost, low availability and dearth of talent. Watch Chandrakana Nandi, our Senior Researcher, debate these contentious aspects with some leaders in this space in the Devcon panel - Future of Smart Contract Security Audits: REKT or WAGMI?
  

• Our Security Engineer Yura Sherman participated in the first Crypto Mondays edition to be held in Warsaw - Are We Safe? Security Landscape of Web3

Past Events

• Certora held a 5K run for code security in Bogota during Devcon. Thank you for joining! Missed it? Certora will hold another run at Barcelona during ETH Gatherings - stay tuned for details!
  

  

• Certora went to ETHWarsaw, the largest event of its kind in the CEE area! Our security engineer Yura Sherman conducted a two-hour hands-on workshop on using formal verification to find bugs in ERC20 smart contracts.
  

  

  Additionally, our developer advocate Uri Kirstein participated in a panel about DeFi Security.

• The entire Certora global team met in Israel for a company offsite. Not only did we get to know each other a little better, we worked to enhance our technology, and plan upcoming product releases.

Future Events

• Join our reverse bug bounty at ETH gatherings with 3K in prizes! Compete to find vulnerabilities and invisible bugs in a smart contract. Limited space - see the details and apply
  

  

• Meet us at Certora’s first event in Southeast Asia - ETH Vietnam!

  

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