Formal verification uses mathematical models and computer algorithms to prove or disprove the correctness of the system’s design with respect to formal specifications expressed as properties.

AAVE started in 2017, which in the world of DeFi, a domain that has been popular since only 2017, is considered OG. Aave, or in its former name ETHLend, started as a P2P lending protocol, but later transformed into a liquidity pool-based protocol in early 2020. Back then, Certora, a small company with major talent and advanced-yet-unripe technology, aspired to enhance the security of an innovative protocol that prioritizes safeguarding against breaches.

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.