This document describes the specification and verification of OpenZeppelin's contracts using the Certora Prover. The work was undertaken from March 2 to April 6, 2022. The latest commit that was reviewed and ran through the Certora Prover was 4088540a.

The scope of this verification is OpenZeppelin's governance system, particularly the following contracts:

ERC20Votes.sol

ERC20FlashMint.sol

ERC20Wrapper.sol

TimelockController.sol

draft-ERC721Votes.sol

Votes.sol

AccessControl.sol

ERC1155.sol

The Certora Prover proved the implementation of the contracts above is correct with respect to formal specifications written by the the Certora team. The team also performed a manual audit of these contracts. The formal specifications focus on validating correct behavior of OpenZeppelin's contracts as described by the OZ team and documentation. The rules verify valid states of a system, proper transitions between states, the solvency of the system and method specifications(unitTest-like rules). The formal specifications have been submitted as a pull request against OpenZeppelin's public git repository.