Solana's token economy runs through a single program. The SPL Token program handles mint creation, token account management, transfers, burns, and delegation for nearly every fungible asset on the network. Weekly token transfers have grown to hundreds of millions, and the SPL Token program is involved in nearly half of all Solana transactions.

P-Token is a Pinocchio-based reimplementation of SPL Token that reduces compute unit consumption by approximately 95%. It is intended as a direct drop-in replacement: existing wallets, DeFi protocols, and programs that call SPL Token should continue to work without modification.

"Drop-in replacement" is easy to say but hard to prove. P-Token introduces a fundamentally different approach to account data loading, several fast-path optimizations, and a number of deliberate behavioral extensions. For backwards compatibility, it must be rigorously proven that the two programs' behaviors agree on all possible inputs across all shared instructions, with caveats as discussed below.

Certora was engaged by the Solana Foundation to formally verify P-Token's equivalence to SPL Token. This post describes what that means, how it was done, and the result of this engagement.

What Does "Equivalence" Actually Mean

Any execution of either program terminates in one of three outcomes: a panic, a return of Ok(()), or a return of Err(e). The verification plan addresses each outcome category independently.

P-Token is not a clone. It deliberately extends SPL Token with new behaviors:

• Delegate self-revocation: P-Token allows the current delegate to call Revoke and clear its own delegation without the account owner signing. SPL Token requires the owner.
• Token-2022 multisig authorities: P-Token's validate_owner accepts multisig accounts owned by Token-2022 in addition to classic SPL Token. SPL Token rejects these.
• Error ordering under malformed accounts: P-Token uses zero-copy account loading that skips full packed validation upfront. When an account carries malformed COption tag bytes, SPL Token rejects immediately with InvalidAccountData. P-Token reaches later instruction logic first and returns a different error depending on the instruction.

These differences make the equivalence relation more natural in one direction. Certora’s formulation is:

• No Panics: Neither SPL Token Program nor P-Token ever panics.
• Equivalence on Ok: If SPL Token returns Ok(()), then P-Token must also return Ok(()). When both return Ok(()), the post-operation account state must be byte-for-byte identical.
• Equivalence on Err: If P-Token returns Err(e), then SPL Token must also return Err(e).

The Equivalence on Ok property follows from P-Token being a superset: any input SPL accepts, P-Token must also accept. The Equivalence of Err captures the guarantee that integrators care about: P-Token cannot introduce new failure modes on inputs SPL Token handles.

The Verification Process

The Certora Prover operates on source code compiled to a low-level intermediate representation, combined with formal specifications written in CVLR (Certora Verification Language for Rust). It uses Satisfiability Modulo Theories (SMT) to reason over all possible inputs simultaneously, producing either a proof of correctness or a concrete counterexample. More information about the tooling is available in the Certora Technology Whitepaper.

The verification harness begins by creating two copies of nondeterministic account_infos and instruction_data that are constrained to be byte-for-byte identical. This allows the Certora Prover to reliably compare the behavior of the two programs across the three outcome categories. The scope covers all instructions shared between SPL Token and P-Token, with the exception of AmountToUiAmount and UiAmountToAmount. Notably, the scope also excludes three new instructions introduced in P-Token: batch , unwrap_lamports and withdraw_excess_lamports .

Certora verified that the No Panics and Equivalence on Ok properties hold for all instructions in scope, requiring no additional assumptions. However, assumptions come into the picture when establishing Equivalence on Err. Specifically: COption tag bytes are assumed to be canonical (0 or 1), and for process_revoke, source_account.delegate is assumed to be unset. Each assumption excludes exactly one of the intentional behavioral differences above. The COption assumption excludes the malformed-account error-ordering cases; the delegate assumption excludes delegate self-revocation. These behaviors are designed, documented, and accepted by the client. The assumptions tell the Prover to stay within the agreed equivalence boundary rather than produce counterexamples the client already knows about.

In summary, no exploitable vulnerabilities were found. All three properties above hold across all instructions in scope. When both programs accept an input, their post-operation account state is byte-for-byte identical. When P-Token rejects an input, SPL Token rejects it with the same error, modulo the three intentional differences.

Why Verification Matters

The findings relevant to the proof assumptions illustrate how formal verification surfaces behavior that is practically invisible to testing.

Error ordering across malformed accounts is the clearest example. When an account with a malformed COption tag such as [2, 0, 0, 0] is passed to most instruction families, SPL Token rejects it during decoding with InvalidAccountData. P-Token's zero-copy loading skips that check and reaches later instruction logic first, producing AlreadyInUse, NotRentExempt, InvalidMint, or IncorrectProgramId depending on the instruction. This mismatch applies across InitializeMint, Transfer, Burn, Approve, CloseAccount, SetAuthority, and more. Discovering this through testing would require constructing the specific malformed inputs for each instruction family. The prover discovers it by covering all inputs.

Delegate self-revocation and Token-2022 multisig each produced concrete counterexamples during proof construction before the corresponding assumptions were added. This is the expected workflow: the counterexample confirms the scope of a known behavioral difference, and the assumption is added to the CVLR specification once the client confirms the behavior is intentional. The assumptions should not be seen as patches on an incomplete proof, but rather formal documentation of design decisions.

Conclusion

P-Token is formally verified to be a correct drop-in replacement for SPL Token across the full shared instruction set. All instructions in scope pass all three equivalence properties. When both programs succeed, their post-operation account state is byte-for-byte identical. When P-Token fails, SPL Token fails with the same error, except in the three cases that reflect intentional design choices.

Read the full report: https://www.certora.com/reports/solana-ptoken