As a part of Certora continuous formal verification activity, we have conducted a formal verification of cbETH token code using our generic ERC20 token specification.
It’s important to note that this is strictly a technical analysis of the smart contract code.
How to look at the dashboard
With Certora technology, we write rules that specify how a smart contract should behave and the tool either proves that the rule always holds or finds a counterexample. It’s impossible to specify general rules for all the ERC20 tokens, since they all have different features. We have chosen to specify a set of strict rules for tokens, for example “supply should always be fixed” and “transfer should always work”. As a result, a token with dynamic supply will obviously fail the fixed supply rule, and a token that has a pause and/or a blacklist function (like USDC) will fail the “transfer should always work”.
In the case of ERC20, the point of these rules is usually to present precise information about the token behavior to the community. This is how we should look at rule failures - usually not as bugs but as information about token features.
Having said that, here is our dashboard with the findings (cbETH is at the bottom of the list):
https://www.certora.com/erc20s/aave-listings/
Here is the rule failures explanation:
- transferCorrect and transferFromReverts rules fail because the token is pausable and transfers don’t work correctly in a paused state.
- otherBalanceOnlyGoesUp rule fails because transferWithAuthorization() and receiveWithAuthorization() change “other’s” balance and they’re not accounted for by our standard spec.
- isMintPrivileged fails because there multiple wallets can get the minter role and mint new tokens by design
- ChangingAllowance rule fails because the permit() function can change allowance and is not part of our standard spec.
In summary, the cbETH token code complies with our generic ERC20 specification and all the rule violations are by design.