Certora and powdr developed a verifier that checks whether autoprecompile optimizations preserve program behavior. Across Keccak and Reth workloads, it proved more than 98% of 6,627 circuit-equivalence checks automatically.

Certora verified the security of Solana's core upgrade from SPL Token to the optimized P-Token program. We used the Certora Solana Prover to prove their equivalence, ensuring that P-Token is a safe drop-in replacement.