Zcash Secures Ironwood Shielded Pool with Formal Verification

Zcash has completed formal verification of its Ironwood shielded pool, a move that rules out undetectable counterfeiting bugs. The network's researchers published over 2,700 machine-checked theorems in Lean programming language to prove balance integrity.

The proof took three teams of researchers and cryptographers more than a month to complete and covers components needed for balance integrity, including zero-knowledge proof system, circuit rules, and ledger-level accounting. However, it does not cover Ironwood's separate privacy guarantees.

Ironwood was introduced through Zcash's NU6.3 upgrade in response to a vulnerability discovered in its Orchard shielded pool that could theoretically have enabled undetectable ZEC counterfeiting.