[Certora] Verification Morpho tokens

colin-morpho commented 3 weeks ago

This PR is a draft of the verification of the Morpho tokens. The verification ensures that the Morpho token is compliant with the ERC20 specification and the delegation of tokens is correct. It patches the OZ specification for ERC20 to support the upgradeable version and the delegation operations. It shows that the Ethereum version is reentrant safe and immutable (up to upgrade).

TODO:

[x] README is updated;
[x] verification succeed;
[x] CI is updated.

anthonyumeh20 commented 2 weeks ago

Confirm

colin-morpho commented 2 weeks ago

Replaced by #90, #91, #92, #93.

morpho-org / morpho-token-upgradeable

[Certora] Verification Morpho tokens #85