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.

Aave V1: A Journey Begins

In January 2020, we started reviewing the already-live V1 protocol. The review began by characterizing the contracts and crafting specifications for the different components and their interactions. This engagement gave the Aave team their first insight into formal verification and its ability to prevent mistakes that would significantly impact the user experience. This marked the commencement of a long and strong partnership between the companies that strengthened Aave’s security on one hand, and the Certora Prover capabilities on the other.

The Early Days: Protecting Aave V2

Eight months passed before Aave started planning a release of their new and improved version of the successful protocol. In the final development phase, Aave contacted Certora and enquired about availability to engage in securing the pre-deployed code, a practice of “shifting left”, which reduces the cost and disruption of security testing by finding code vulnerabilities earlier. Flattered by the offer and with significant improvement to our methodology, experience and technology, we accepted the job with the hunger to prove the effectiveness of formal verification in smart contract security.

Over the next quarter, we worked closely with the development team to better understand and formally characterize the system. Being a top team that puts security as the highest priority, Aave patiently and eagerly collaborated with us, and results were quick to arrive. The review, which included 20 contracts containing over 5,500 lines of code, produced ten significant unique bugs discovered by Certora. Identifying these vulnerabilities in the code before deployment prevented impacts ranging from incorrect totalSupply reporting to the loss of assets. The effort also produced a total of 25 specification rules that were integrated into CI (continuous integration checks). As a result, Aave V2 has indeed proven its resilience over time.

Since its deployment in November 2020, the protocol has held billions of dollars without being compromised, with a peak TVL of over 18 billion dollars.

Continuing The Journey: Protecting Aave V3

After another year, in November 2021, Aave was ready again to release a new and improved version of the protocol. V3 held great potential by promising considerably greater capital efficiency, a wider variety of risk and control mechanisms, and additional highly anticipated features. For the extremely critical mission of reviewing the code and searching for vulnerabilities, Aave engaged with no less than six different top security firms, among them Certora.

The previous year, the Certora Prover gained some critical new capabilities. Our security experts formally verified a set of well-thought specification rules for two months. The high complexity made the reviewing effort slower and harder and forced us to verify only a subset of contracts. Nevertheless, we implemented 45 specification rules on chosen contracts and found five significant bugs in the code, which Aave fixed before deployment.

The protocol has since been deployed on various L2 chains and later on the Ethereum mainnet. So far, with over two billion dollars in TVL, the protocol proves its immunity.

Continuous Security and Agility: Present Days

In March 2022, with great history and understanding between Aave and Certora, we turned to the DAO to offer our services. The proposal included dedicated security consulting assisted by the usage of the Certora Prover technology and full responsibility for building and managing a security community that reviews code through the formal verification approach. Following great support from the DAO, a new era began. In the following half year, we had the honor of being a part of the development process for huge contracts such as:

• The aStETH, which holds around 1 Billion dollars in TVL
• Critical governances V2 bridges to several L2 chains
• The AAVE Token V3, which plays a central role in the V3 governance system

After a successful contribution period, the DAO decided to extend its use of our services by another year. Since then, we feel that we have played an integral role in securing some of the most critical moves and components of the protocol:

• The deployment of V3 to Ethereum mainnet, which currently holds over 2 Billion dollars
• The deployment of the Gho token, which despite being in its early days is already backing over 18 million dollars worth of assets
• The upgrade of the safety module, which holds over 300 million dollars worth of AAVE tokens as insurance for the protocol
• And more

During this era of continuous contribution and partnership, we:

• Reported 12 significant bugs that prevented the potential loss of billions of dollars to the protocol and its users
• Reviewed over 120 contracts containing over 40,000 lines of code, wrote over 800 specification rules and verified them on every code addition via hundreds of CI runs
• Held and managed six community efforts to secure critical smart contracts, while empowering the Aave community to contribute to scalable secure development, handing nearly $400,000 in rewards to incentivize quality specification writing and bug finding.

Along the road of contribution to the protocol, we held countless discussions with developing entities regarding the design and implementation of various contracts. We pushed the developers to better understand their code and design by raising questions and requiring coherent answers. We escorted development by being constantly available, consulting with them on any matter needed, big or small, in a short time and with full professionalism, be it a review of a token listing payload, a review of a massive critical new component, or an incident response. Our consulting created a direct development feedback loop that organically improved the design and security of the code for current and future releases.

During the engagement with the DAO, we supplied Aave with continuous security of the highest quality while allowing agile, smart contract development that promotes protocol prosperity.

Stats For Nerds

Among other things we:

• Reviewed 169 smart contracts containing 51,289 lines of Solidity code (our technology analyzes the bytecode, which is significantly larger)
• Prevented 28 significant bugs before deployment over our long collaboration with AAVE
• Reported six additional significant bugs on numerous contracts currently under development
• Increased the cadence of development by providing a weekly rapid response
• Wrote formal properties (can be found here) and used the Certora Prover technology for formally checking the code for most of the code
• Allocated $383,500 for external security researchers to review the code using the Certora Prover on 6 different efforts

We consult Aave and BGD on live incidents, a tricky task for DeFi protocols of the magnitude of Aave. In one particular incident, our team was able to dispute a white hacker’s potential exploit quickly and save the DAO money and introduction of malicious code, which is always a potential hatch for security breaches. We also presented BGD with several potential live threats and discussed possible patches.

Conclusion: A Collaborative Legacy

Aave is one of the most successful protocols in DeFi today. However, it is also one of the most complex lending systems in the entire web3 eco-space. Its complexity, along with its high TVL growth, escalates security risks and necessitates engaging with top security professionals.

Certora utilizes expert security researchers that are specialized in the Aave code base. Our continuous engagement provides security consultancy for every aspect of Aave security with almost immediate availability, including incident responses. We improve the protocol’s design by shifting the developer’s approach towards designing with specification and security in mind, which puts to paper the expected behavior of the system and the underlying assumptions which are being used across the code.

Our formal verification technology lowers smart contract risks. Formal verification generates generalized and powerful specification tests that can be re-used to check every introduction of new code to the protocol, thus preventing the deployment of new vulnerabilities.