Certora Formally Verifies Solana’s P-Token Upgrade as Equivalent to SPL Token

Even as P-Token frees up to 98% more compute units, Certora proves that it still delivers byte-for-byte compatibility with SPL Token with no vulnerabilities found.

Pablo

Published:
Edited:

Solana's recently deployed P-Token upgrade represents one of the most significant infrastructure changes in the network's history. The upgrade dramatically reduces the compute resources required for token operations while preserving compatibility with the existing SPL Token program.

To validate that claim, the Solana Foundation engaged Certora to conduct a formal verification to prove behavioral equivalence between the legacy SPL Token implementation and the new Pinocchio-based P-Token program. Research and development firm Anza has previously described formal verification as “the strongest guarantee” of P-Token’s equivalence, and Certora’s results provide a further validation for P-Token's role as a “drop-in” replacement for one of Solana's most widely used programs.

Why the Token Program Matters

The SPL Token program sits at the center of Solana's token economy. It handles mint creation, token account management, transfers, burns, and delegation for the vast majority of assets on the network. Because nearly every non-voting transaction on Solana interacts with tokens in some form, any change to the token program carries broad implications for the ecosystem.

P-Token introduces a new implementation built on the Pinocchio Rust library. The upgrade delivers substantial performance improvements, reducing compute consumption by approximately 95-98% for many common operations. Standard token transfers, for example, fall from 4,645 compute units to only 76, while transfer_checked instructions decrease from 6,200 compute units to 105.

These efficiency gains can free an estimated 12-13% of block space across the network, creating additional capacity without increasing block limits.

The Challenge of Proving a “Drop-In” Replacement

While performance improvements attract attention, compatibility remains the most important requirement for an infrastructure upgrade of this scale. Existing wallets, dApps, protocols, and smart contracts rely on the behavior of the SPL Token program. Any unexpected deviation could cause integration issues or pose risks to developers and users.

P Token

P-Token does not simply copy the original codebase. The new implementation adopts a different architecture, including zero-copy account access, optimized execution paths, and additional functionality. As a result, developers could not rely solely on conventional testing to establish compatibility.

Instead, Certora used formal verification techniques to mathematically analyze whether the two programs behave the same way across all possible inputs within the defined verification scope.

What Does Equivalence Mean for P-Token?

Certora's verification framework evaluated three outcome categories for each instruction analyzed.

First, neither program should ever panic during execution; i.e., the program must never crash or abort due to a bug, edge case, etc.
Second, if the SPL Token program successfully processes an instruction and returns Ok(()), P-Token must also return Ok(()). In those cases, both programs must leave account data in a byte-for-byte identical state after execution.
Third, if P-Token returns an error, the SPL Token program must return the same error under the same conditions.

Certora’s framework ensures that for every possible input account state and instruction, the program either succeeds (Ok(())) or fails gracefully (Err(e)), but never crashes internally. P-Token's implementation is designed as a superset of SPL Token functionality, meaning any operation accepted by SPL Token must also be accepted by P-Token.

The verification effort identified several deliberate differences between the two programs. P-Token allows delegate self-revocation, enabling a delegate to revoke its own authority without requiring the token account owner to sign the transaction. SPL Token requires the owner's signature for the same action.

P-Token also expands support for Token-2022 multisig authorities. While SPL Token rejects these accounts, P-Token accepts them.

A third difference involves error handling when malformed account data contains noncanonical COption tags. SPL Token immediately rejects such accounts with an InvalidAccountData error. P-Token's optimized account loading process reaches deeper into the instruction logic before generating an error, which can produce different results depending on the instruction being executed.

Because these differences were intentional and documented, Certora incorporated assumptions into portions of the verification process to keep the analysis focused on the agreed compatibility boundary.

How the Verification Worked

Certora's Prover analyzes source code after compilation into a low-level intermediate representation. Engineers then write formal specifications using the Certora Verification Language for Rust, known as CVLR.

The verification harness created identical copies of account information and instruction data, allowing the prover to compare both programs under the same conditions. Using Satisfiability Modulo Theories techniques, the system evaluated all possible inputs simultaneously rather than relying on a limited collection of test cases.

The scope included every instruction shared between SPL Token and P-Token, excluding AmountToUiAmount and UiAmountToAmount. The review also excluded the three new P-Token specific instructions: batch, unwrap_lamports, and withdraw_excess_lamports.

Throughout the process, the prover either generated a proof of correctness or produced concrete counterexamples highlighting behavioral differences requiring review.

Findings and Results

Certora reported that no exploitable vulnerabilities emerged during the verification effort. The analysis confirmed that the No Panics and Equivalence on Ok properties hold across all instructions within scope without requiring additional assumptions. The Equivalence on Error property also holds across the shared instruction set when accounting for the three intentional behavioral differences previously identified.

Most importantly, the verification demonstrated that whenever both programs successfully process the same input, they produce byte-for-byte identical post-operation account states. The process also highlighted how formal verification can uncover edge cases that traditional testing may miss.

A Significant Milestone for Solana Infrastructure

The verification results arrive shortly after P-Token's deployment to mainnet, providing additional confidence in one of Solana's most consequential infrastructure upgrades.

By combining major compute savings with formally verified behavioral equivalence, the upgrade seeks to improve network efficiency without disrupting the applications and assets that depend on the token program every day.