Zcash says Ironwood proof rules out undetectable counterfeiting bugs
Summary
Zcash researchers completed a machine-checked Lean proof for Ironwood, the new shielded pool introduced in NU6.3. The proof spans over 2,700 theorems and was finished by three teams in about a month. It establishes “balance integrity”: under stated cryptographic assumptions, the pool cannot create or pay out more value than has publicly entered it. The proof covers the zero-knowledge proof system, circuit rules, and ledger accounting, but not privacy guarantees. Ironwood was built after a vulnerability was found in Orchard that could have allowed undetectable ZEC counterfeiting, though no exploitation was detected. A public “turnstile” checkpoint helps prevent excess coins from moving into Ironwood.
