区块链安全公司Certora近日完成了对Solana代币扩展的正式验证审查，使用其深度形式验证工具对代码关键属性进行了规范编写和验证。Certora团队的主要发现包括：识别出一项可将程序性能提升20%的优化机会；开发了验证Solana团队近期更新的规则，以加强现有安全措施；编写了可重用的规范，用于验证多个指令，发现了之前所有审计人员都未察觉的问题。

具体而言，Certora建议不使用sol_memcmp，而采用Rust提供的平台无关比较方法，这一改进使TransferChecked指令的计算单元减少了约20%。

此外，Certora的验证还发现并确认了一个涉及未经检查转账和经过检查转账一致性的问题的修复。

最后，团队发现烧毁指令（Burn和BurnChecked）中缺少针对转账指令实施的修复，这一问题已得到SPL开发者的确认并修复。