This report describes the specification and the verification of Balancer’s contract TimelockAuthorizer using the Certora Prover. The latest commit reviewed and ran through the Certora Prover was 36465b52. The scope of our verification was the following contracts:

TimelockAuthorizer.sol

TimelockAuthorizerManagement.sol

The Certora Prover proved that the implementation of the contract above is correct with respect to formal specifications written by the Certora team. The team also performed a manual audit of these contracts. The formal specifications focus on validating the correct behavior of the contracts above as described by the Balancer team and the contract documentation. The rules verify valid states of the system, proper transitions between states, method integrity, and high-level properties (which often describe more than one element of the system and can even be cross-system).