TechFlow reports that blockchain security firm Certora recently completed a formal verification review of the Solana token extension, using its advanced formal verification tools to specify and verify critical code properties. Key findings from the Certora team include: identifying an optimization opportunity that could improve program performance by 20%; developing verification rules for recent updates made by the Solana team to strengthen existing security measures; and creating reusable specifications to validate multiple instructions, uncovering issues previously missed by all prior auditors.
Specifically, Certora recommended replacing sol_memcmp with Rust's platform-independent comparison method, an improvement that reduces the compute units of the TransferChecked instruction by approximately 20%.
In addition, Certora’s verification identified and confirmed a fix for an issue concerning consistency between unchecked and checked transfers.
Finally, the team discovered that the burn instructions (Burn and BurnChecked) were missing a fix previously implemented in transfer instructions. This issue has been acknowledged and resolved by the SPL developers.
