Overly Optimistic Optimizer — Certora Bug Disclosure

John Toman, VP of R&D at Certora, discovered a previously unknown optimization bug in the Solidity compiler (version 8.14 and lower). This bug causes the optimizer to consider some memory operations in inline assembly as being "dead" and…

Post-Mortem Analysis of the Notional Finance Vulnerability — A Tautological Invariant

Stopping DeFi Bugs at Scale

Certora empowers smart contract developers to detect and prevent billion-dollar mistakes before deploying code…

Detecting Corner Cases in Compound V3 with Formal Specifications

We describe an interesting…

Incorrect Calldata Validation in Inter-Contract Communication — Certora Bug Disclosure

Five Myths about Formally Verifying Smart Contracts

For a long time it puzzled me how something so expensive, so leading…

Finding Bugs in Formal Specifications

Formal verification can drastically improve code security when done right. However, it can…

Avoided Solidly Voting System Manipulation

A bug found in a past version of Solidly, enabling an…

Shift Left: Formal Verification First, Not Last!