This document describes the specification and verification of Balancer's contracts using the Certora Prover. The work was undertaken from June 21st to September 23rd. The latest commit that was reviewed and run through the Certora Prover was commit af9e9eb.

The scope of our verification was the following contracts and their various components:

[ ComposableStablePool.sol ]

[ StablePool.sol ]

[ WordCodec.sol ]

The Certora Prover proved the implementation of the Balancer contracts is correct with respect to the formal rules written by the Balancer and the Certora teams. During the verification process, the Certora Prover discovered bugs in the code listed in the table below. Additionally the code was manually reviewed by two researchers from Certora.