Zcash turns to formal verification to prevent undetectable counterfeiting bugs

Zcash developers are using formal verification for the upcoming Ironwood network upgrade and shielded pool to rule out undetectable counterfeiting bugs after a recently disclosed vulnerability in Orchard exposed the limitations of relying on conventional code audits, as explained by developer and crypto researcher Sean Bowe in a Tuesday blog post.

Ironwood is designed to address an accounting flaw discovered in the Orchard shielded pool and restore confidence in the cryptocurrency’s supply integrity. The flaw was discovered by Shielded Labs researcher Taylor Hornby and patched before any known exploitation.

According to the developers, undetectable counterfeiting can only arise from flaws in a protocol’s mathematical specification or from broken cryptographic assumptions, while implementation bugs always leave evidence that can be detected by replaying the blockchain with corrected software.

The team said its formal verification effort focuses on proving the correctness of Ironwood’s cryptographic specification rather than auditing implementation code, arguing this is sufficient to rule out undetectable counterfeiting bugs under standard cryptographic assumptions.

The work is being carried out with contributors from zkSecurity and the Zcash Open Development Lab using the Lean theorem prover alongside traditional audits and AI-assisted analysis.

Expected to activate in July 2026, Ironwood will close the old shielded pool and launch a corrected replacement. Users will migrate funds through a “turnstile” mechanism designed to help demonstrate that no counterfeit ZEC entered circulation while eventually capping the amount of value remaining in Orchard.