OpenZeppelin Contracts
OpenZeppelin
June 13, 2022
This report describes the specification and verification of OpenZeppelin's contracts using the Certora Prover. The work was undertaken from May 9th to June 10th. The latest commit that was reviewed and run through the Certora Prover was commit 109778c.
The scope of our verification was the following contracts:
The Certora Prover proved the implementation of the OpenZeppelin contracts is correct with respect to the formal rules written by the OpenZeppelin and the Certora teams. During the verification process, the Certora Prover discovered bugs in the code listed in the table below. All issues were promptly corrected, and the fixes were verified to satisfy the specifications up to the limitations of the Certora Prover. The Certora development team is currently handling these limitations. The next section formally defines high level specifications of OpenZeppelin. All the rules are publicly available in a public github.
