Zcash activates Ironwood upgrade, backs $1.7B shielded pool with formal proof
Tech & Launches ·
The new shielded pool, rolled out as part of NU6.3, now carries a machine-verified mathematical guarantee against undetectable counterfeiting rather than relying solely on manual code audits.
Zcash's Ironwood upgrade went live with roughly $1.7 billion held in the shielded pool, according to coindesk.com. Alongside the activation, developers published a completed formal verification effort covering the pool's core security guarantee, known as balance integrity, as detailed on tachyon.z.cash.
The verification takes the form of a machine-checked proof written in the Lean proof assistant, comprising more than 2,700 theorems and requiring well over a month of work from three separate teams of researchers and cryptographers. Rather than depending on human review of code to catch mistakes, the proof mathematically demonstrates that Ironwood's zk-SNARK system satisfies knowledge soundness — meaning a party generating a shielded transaction must actually possess valid hidden data justifying it, not merely produce a proof string that happens to pass verification. Most of the verification work centered on this property, since ordinary soundness checks are considered inadequate for shielded systems where hidden transactions could otherwise admit false justifications.
Balance integrity, the umbrella property the proof establishes, also touches several other protocol components beyond the SNARK itself, with each dependency traced down to explicitly named assumptions rather than left implicit. The approach models provers algebraically, requiring that any output tied to hidden transaction data can be traced back through known mathematical representations, which lets the extraction of a valid witness happen without the runtime blowups that have made traditional soundness proofs impractical for protocols built on inner product arguments at comparable security depth.
The rollout has been corroborated across multiple reports describing both the shielded pool's $1.7 billion size and the Ironwood activation itself, with additional accounts indicating the update also addressed vulnerabilities tied to the Orchard privacy pool and introduced a tool aimed at detecting counterfeit ZEC.
Left unaddressed in the material is how the counterfeit-detection tool functions in practice, what specific Orchard vulnerabilities were remedied, and whether independent auditors outside the original verification teams will review the Lean proof. It also remains to be seen whether the $1.7 billion figure shifts materially as users migrate funds into or out of the newly verified pool following activation.