The Deferred Check
It was found in p-token before mainnet. Here's how.
Hey, it’s Arsen.
In today’s menu:
• A p-token vulnerability was discovered — batch instruction + deferred ownership = inflated wrapped SOL
• OpenZeppelin goes continuous — what their new model signals for the industry
• Vitalik on formal verification: what it actually proves, and where it breaks
• And more…
🐛 Vulnerability
p-token: batch instruction breaks the deferred ownership invariant
p-token is Pinocchio-based. A compute-optimized rewrite of Solana’s SPL token program. Transfers now cost over 95% fewer CUs.
One of the CU savings: skipping explicit ownership checks on source accounts during transfers. The logic holds — any write to a foreign-owned account fails at the runtime level. The check is redundant.
What breaks that assumption?
The batch instruction.
Batch lets callers bundle multiple token operations into a single program call. Inside that single call, state changes can be reversed before the runtime check runs.
Here’s the mechanic:
Create a fake wrapped SOL account you control. Set the mint to native mint. Set is_native to None. Send a batch:
Transfer X wrapped SOL from the fake account → target
Transfer X wrapped SOL from a real account → back to the fake account
At the end: the fake account’s data is unchanged. The runtime check never triggers. The target’s amount field has increased. No lamports moved.
Any DeFi protocol that treats amount as the source of truth for collateral or flash loan repayment is exploitable from there.
The Anza team fixed it quickly — explicit ownership checks added to the batch handler for any instruction that modifies accounts.
The lesson: deferred runtime checks are a valid optimization when instructions execute independently. Batch breaks that assumption by allowing multiple state transitions inside a single invocation — including ones that undo the write the runtime was waiting to catch.
Individually safe optimizations can become vulnerabilities when composed with new functionality.
🗞️ News
OpenZeppelin launches Continuous Security Program
OpenZeppelin announced a subscription-based, always-on security model. Not point-in-time audits — continuous coverage across the full development lifecycle.
The core premise: most major onchain hacks don’t come from bugs that audits missed. They come from code shipped between audits. Upgrades, new integrations, parameter changes — pushed to production without security review.
Their model is structured around four areas: Architect, Build, Secure, Support. Continuous loops, not sequential phases. AI-augmented scanning plus senior researcher review.
What this signals:
The point-in-time audit isn’t being replaced — it’s being framed as one layer, not the full stack. For large, fast-moving protocols, that framing is probably correct.
The market OpenZeppelin is targeting is institutional — Fidelity, DTCC, WisdomTree-tier clients. Not the same market as competitive audits or private engagements.
But the tooling bar it sets is real. Their AI Auditor reportedly surfaces a high or critical finding in one of every three scans. That’s the baseline expectation for continuous coverage now.
📚 Education
Formal verification: what it proves, and where it breaks
Vitalik published a deep dive on formal verification. The part most useful for auditors is buried about halfway through.
“Provably correct” doesn’t mean what it sounds like.
Formal verification proves that multiple specifications of intent are compatible with each other. It does not prove that those specifications match what users actually expect.
The model:
Code = one expression of intent
Type system = another expression
Test suite = another expression
Formal proof = another expression
The more ways you express the same intent, the harder it is for bugs to survive undetected. FV extends that redundancy further than any test suite can — you can verify an optimized implementation against a readable reference, check ten mathematical properties simultaneously, and use AI to do all of it efficiently.
Where it breaks down:
When only part of the code is verified and the unverified parts are where the bugs live. When the specification is wrong. When the proof assumes something the hardware doesn’t guarantee. Vitalik documents real examples: a formally-verified C compiler generating wrong assembly for edge cases. A Signal protocol proof that holds until hardware leaks through side channels.
The real takeaway: more redundant specifications of intent, automatically checked, is always better. FV is a powerful accelerant of that direction — not a final answer.
For auditors: FV is increasingly relevant for infrastructure (STARKs, ZK-EVMs, consensus). For program-level work, tests plus invariants plus manual review is still the realistic model. But the infrastructure you’re auditing against is being formally verified — understanding what that means, and what it doesn’t cover, matters.
That’s it for this week.
Reply with the Solana bug, tool, or pattern you want me to cover next — I read every one.
If a working Solana auditor in your circle would find this useful, forward it their way.
— Arsen, working Solana auditor