The Certora team performed a manual audit of all the Solana contracts. During this process, the team discovered bugs in the smart contracts code, as listed on the following pages. 

The Certora Prover demonstrated that the implementation of the Solana contracts above is correct with respect to the formal rules written by the Certora team. Please note that a few more formal rules are not included in this report, as they were proven with an unreleased version of the Certora Prover. Once those rules are proven on a released version of the Certora Prover, we will add them to the next version of this document.