Solana Foundation's P-Token is a Pinocchio-based implementation of the SPL Token program, intended to preserve SPL Token semantics while reducing compute overhead. It keeps the core token flows around mints, token accounts, authorities, delegation, and native SOL, while adding P-Token-specific instructions such as Batch, WithdrawExcessLamports, and UnwrapLamports.

This document describes the specification and verification of P-Token's equivalence to SPL Token using the Certora Prover.