2,700 Theorems Prove Zcash Ironwood Immune to Undetectable Counterfeiting

Woofun AI reports that Zcash’s Ironwood upgrade has been formally verified by Project Tachyon, confirming the absence of undetectable counterfeiting bugs in its new shielded pool. This machine-checked proof establishes critical security assurances for the network’s latest cryptographic implementation.

The verification effort, concluded on Tuesday, utilized the Lean programming language to construct a proof comprising over 2,700 theorems. Three teams of researchers and cryptographers spent more than a month validating balance integrity, ensuring the shielded pool cannot distribute more value than publicly entered.

Woofun AI data shows the scope covers Ironwood’s zero-knowledge proof system, circuit rules, and ledger-level accounting, though separate privacy guarantees remain outside this specific verification.

Structurally, the proof isolates the components necessary to prevent value inflation within the new pool.

Ironwood was deployed via the NU6.3 upgrade to address a vulnerability in the Orchard shielded pool that theoretically allowed undetectable ZEC counterfeiting. Zcash developers stated there is no evidence the flaw was exploited, aiming to restore confidence in supply integrity. The new architecture replaces the compromised Orchard pool, mitigating the risk of hidden inflation while maintaining the network’s operational continuity.

Funds migrating from Orchard must pass through a public accounting checkpoint called a turnstile, designed to block any hypothetical excess coins from entering Ironwood. As assets leave the old pool, this process provides growing evidence regarding whether Orchard was previously exploited. This mechanism serves as a final audit trail for the legacy system’s integrity.