Zcash researchers have completed formal verification of the network’s Ironwood shielded pool, publishing a machine-checked proof that excludes undetectable counterfeiting bugs under its stated cryptographic assumptions. The work establishes that the new pool cannot distribute more value than has publicly entered it.

The proof, prepared in the Lean programming language, contains more than 2,700 theorems and required more than a month of effort by three teams of researchers and cryptographers. It addresses the components required for balance integrity, including the zero-knowledge proof system, circuit rules and ledger-level accounting. Privacy properties of Ironwood fall outside the scope of the verification.

Ironwood was introduced in the NU6.3 network upgrade following discovery of a vulnerability in the preceding Orchard shielded pool. That flaw could in theory have permitted undetectable creation of ZEC tokens. Developers reported no evidence that the issue had been exploited. The new pool aims to reinforce confidence in the integrity of the token supply.

Assets moving from Orchard into Ironwood must pass through a public accounting checkpoint known as a turnstile. The mechanism is intended to block any hypothetical excess coins from entering the new pool. As balances exit Orchard, the process may also generate additional evidence regarding whether the earlier pool was compromised.