Trong tin tức gần đây từ TechFlow, công ty bảo mật blockchain Certora đã hoàn thành việc xem xét xác minh chính thức của tiện ích mở rộng mã thông báo Solana. Họ đã sử dụng công cụ xác minh hình thức sâu để viết và xác minh các thuộc tính mã chính. Các phát hiện chính của đội ngũ Certora bao gồm: xác định cơ hội tối ưu hóa có thể cải thiện hiệu suất chương trình lên đến 20%; phát triển các quy tắc để củng cố các biện pháp bảo mật hiện có cho các cập nhật gần đây của Solana; viết các đặc tả có thể tái sử dụng để xác minh nhiều hướng dẫn, phát hiện các vấn đề trước đó không được chú ý bởi tất cả các kiểm toán viên. Cụ thể, Certora khuyến nghị không sử dụng sol_memcmp mà thay vào đó nên áp dụng phương pháp so sánh độc lập với nền tảng của Rust, giảm đơn vị tính toán của hướng dẫn TransferChecked khoảng 20%. Hơn nữa, xác minh của Certora cũng phát hiện và xác nhận một sửa lỗi cho vấn đề nhất quán liên quan đến các chuyển giao không kiểm tra và chuyển giao kiểm tra. Cuối cùng, đội ngũ đã phát hiện ra thiếu sửa lỗi cho các hướng dẫn chuyển giao trong các hướng dẫn đốt (Burn và BurnChecked), điều này đã được nhà phát triển SPL công nhận và sửa lỗi.