May 31, 2021
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.
May 27, 2021
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.
April 12, 2022
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.
August 14, 2023
The Vyper programming language provides a clean memory and control abstraction. In comparison to Solidity, it is considered highly attractive for DeFi programming.
May 30, 2021
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.
June 15, 2022
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.
June 2, 2021
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.
April 28, 2025
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.
September 9, 2024
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.
October 18, 2022
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.
February 17, 2025
Safeguard is a Geth extension that monitors Ethereum protocol invariants in real time to enhance the security of DeFi systems and monitor exploits.