The Certora Prover demonstrated that the implementation of the Yul contracts above is correct with respect to the formal rules written by the Certora team. In addition, the team performed a manual audit of all the Yul contracts. During the verification process and the manual audit, the Certora team discovered issues in the Yul contracts code, which can be found in the report.