Certora has completed the formal verification of the Solana token extension, uncovering multiple optimizations and security improvements.

In recent news from TechFlow, the blockchain security company Certora has completed a formal verification review of the Solana token extension. They used their deep formal verification tool to write and verify key code properties. The main findings of the Certora team include: identifying an optimization opportunity that can improve program performance by 20%; developing rules to strengthen existing security measures for Solana's recent updates; writing reusable specifications to verify multiple instructions, uncovering issues that were previously unnoticed by all auditors. Specifically, Certora recommends not using sol_memcmp but adopting Rust's platform-independent comparison method, which reduces the computational units of the TransferChecked instruction by about 20%. Furthermore, Certora's verification also discovered and confirmed a fix for a consistency issue involving unchecked transfers and checked transfers. Finally, the team found a lack of fixes for transfer instructions in the burn instructions (Burn and BurnChecked), which has been acknowledged and fixed by SPL developers.