Zcash researchers have formally verified Ironwood, publishing a machine‑checked proof that the network’s new shielded pool cannot create undetectable counterfeit transactions under its cryptographic assumptions. The proof, written in the Lean programming language, consists of more than 2,700 theorems and was completed by three research teams over a month, according to Project Tachyon. It establishes balance integrity, ensuring that the shielded pool cannot pay out more value than has entered it, and covers the zero‑knowledge proof system, circuit rules and ledger accounting, but does not address Ironwood’s privacy features. Ironwood was introduced in the NU6.3 upgrade to address a vulnerability in the Orchard shielded pool that could have allowed undetectable ZEC counterfeiting. Developers said they found no evidence that the flaw had been exploited. The new pool requires funds moving from Orchard to pass through a public turnstile checkpoint, which prevents excess coins from entering Ironwood and may provide evidence of any prior exploitation. The verification does not constitute a judgment on whether the Orchard vulnerability was used, and Zcash continues to monitor the network.