The Certora Prover demonstrated that the implementation of the Solana contracts above is correct (modulo identified issues) with respect to the formal properties formulated and written by the Certora team. In addition, the team performed a manual audit of all the Solana contracts. During the verification process and the manual audit, the Certora team discovered bugs in the protocol code, as listed on the following pages.