证明P-Token：Solana Token程序升级的形式化验证 P-Token是SPL Token的Pinocchio重实现，减少约95%计算单元消耗，作为直接替代品。Certora使用形式化验证证明P-Token与SPL Token在共享指令上的等价性：无panic、成功时状态字节一致、失败时错误相同（除三个有意行为差异）。验证覆盖所有共享指令，未发现可利用漏洞。 形式化验证 P-token SPL Token Certora 等价性 Solana Certora 发布于 2026-06-04 91 0 0
