Zcash Verifies Ironwood Network with Over 2,700 Machine-Checked Theorems

Zcash has completed formal verification of its Ironwood network, publishing a proof that rules out undetectable counterfeiting bugs. The proof, written in Lean programming language, comprises over 2,700 machine-checked theorems and took three teams of researchers and cryptographers more than a month to complete.

The new shielded pool was introduced through Zcash's NU6.3 upgrade after a vulnerability was discovered in its Orchard shielded pool that could have enabled undetectable ZEC counterfeiting. However, developers found no evidence that the flaw had been exploited.

The proof covers the components needed for balance integrity, ensuring the shielded pool cannot pay out more value than has publicly entered it. It does not cover Ironwood's separate privacy guarantees.