Dear Aave community,
At Formal Land, we specialize in Web3 security through advanced formal verification techniques. This enables showing that a smart contract is free of classes of vulnerabilities by covering all possible inputs.
We recently developed the open-source tool coq-of-solidity to simplify the formal verification of Solidity programs using the generic verification system Coq.
Here is a general presentation that we made: coq-of-soldity slides
Utility
With this tool, one can check the properties and invariants of Aave’s smart contracts for every possible input. As the Coq proof system is an interactive theorem prover, virtually any property is expressible and verifiable. An example of such a property is showing the backward compatibility between two successive versions of the protocol, meaning that for any valid input for version A, we always get the same result for version B.
This would complement the verification work testing techniques or other formal verification tools such as Certora.
Plan
The plan is as follows:
- Formally verifying that the code of Aave is equivalent to an idiomatic Coq version using
coq-of-solidity
. - Showing this idiomatic version to be equivalent to a more high-level version relying on abstract primitives such as identity, token, ownership, …
- Formally verifying general properties about this high-level version, such as the absence of stealing, blocked state, rounding errors, etc…
Time estimate
We estimate that the whole process above will take around six months for a two-person team. We designed coq-of-solidity
so that the resulting verification can be integrated into the CI system. In particular, when the code changes, the verification of properties for the parts that did not change still works.
As a result, we will get more confidence that the smart contracts are free of vulnerabilities and that the protocol is secure.
We are happy to hear about what you think about this project. Additional links: