This document describes the specification and verification of the sidechain bridge of the Milkomeda protocol using the Certora Prover. The work was undertaken from 07/09/2022 to 12/10/2022. The latest commit that was reviewed and run through the Certora Prover was ce5827a. The scope of our verification was the SidechainBridge contract.

The Certora Prover verified that the implementation of the sidechain bridge is correct with respect to the formal rules written by the Certora team. During the verification process, the Certora Prover discovered bugs in the code listed in the table below. The development team at dcSpark promptly corrected all issues, 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 the high level specification of Milkomeda's sidechain bridge.