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.

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