The Ethereum Object Format (EOF) proposal removes dynamic jumps to make smart contract bytecode more predictable and analyzable. Some critics argue that easier static analysis offers limited value, but we disagree. Static analysis tools have already prevented countless costly bugs. Simplifying EVM control flow could pave the way for safer contracts and better tooling. Security must be a central factor when shaping Ethereum’s future.

Formal verification improves software security by finding bugs and mathematically proving their absence via mathematical methods. Smart contracts are perfect applications for formal verification because bugs are costly, the code is typically small or modular, and it evolves over time.

Certora uncovered a Solidity compiler bug affecting inter-contract calldata validation in versions ≤0.8.13. The bug allowed malicious inputs to corrupt external calls, posing serious security risks.

The Vyper programming language provides a clean memory and control abstraction. In comparison to Solidity, it is considered highly attractive for DeFi programming.

We’ve been working on a compiler equivalence checker named Concord. Given two programs, Concord uses the existing Certora Prover infrastructure to prove that the programs are equivalent on all inputs.

Certora uncovered a serious Solidity bug (fixed in v0.8.0) where maliciously crafted storage fields could exploit abi.encodePacked, causing unexpected memory exposure and non-determinism in Ethereum smart contract transactions.

Certora identified and disclosed a significant optimization bug affecting Solidity compiler versions ≤0.8.14, where crucial memory operations in inline assembly could be erroneously removed, potentially impacting smart contract correctness.

Concordance is an open-source tool that uses LLMs to automatically rewrite heavily optimized Solidity (including inline assembly) into clear, readable code while preserving all observable on-chain behavior. Each rewrite is proven equivalent by Concord, the equivalence checker, so audits get easier without sacrificing correctness.

During Aave V3’s deployment on ZKsync, a severe LLVM compiler bug was discovered—one that could lead to fund loss. Learn how Certora, Aave Labs, BGD Labs, and Matter Labs traced the issue to its root cause and uncovered a hidden risk in compiler optimizations.

Safeguard is a Geth extension that monitors Ethereum protocol invariants in real time to enhance the security of DeFi systems and monitor exploits.

Certora discovered a critical Solidity compiler bug (fixed in 0.6.5) enabling memory corruption through overflow in dynamically sized arrays. Understand the bug’s details and impact.

Certora uncovered a severe Solidity compiler bug (≤0.8.3) allowing maliciously crafted byte buffers to violate memory isolation during ABI deserialization. This vulnerability enabled attackers to access unintended memory regions or inject non-deterministic behavior into smart contracts.

Certora identified a serious bug in Solidity compiler 0.7.3 silently corrupting storage when handling zero-length bytes arrays, resulting in increased gas costs and potential data inconsistencies.