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 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 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.

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.

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.

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.

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.

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.

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.

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