Zcash adopts formal verification for Ironwood upgrade

2 min read

Zcash developers moved to formal verification for the Ironwood network upgrade after a recently disclosed accounting flaw in the Orchard shielded pool revealed limits of conventional audits. The flaw, found by Shielded Labs researcher Taylor Hornby, was patched before known exploitation. The team says undetectable counterfeiting stems from specification or cryptographic assumption flaws, not implementation bugs, and is focusing proofs on Ironwood's cryptographic specification using the Lean theorem prover with contributors from zkSecurity and the Zcash Open Development Lab. Ironwood will close the old shielded pool, launch a corrected replacement, and use a turnstile migration to demonstrate supply integrity when it activates in July 2026.

Ironwood will formal-verify specs to prevent undetectable counterfeiting.