Zcash Verifies Ironwood Shielded Pool with 2,700 Theorems

Zcash researchers have completed formal verification of Ironwood, publishing over 2,700 machine-checked theorems that rule out undetectable counterfeiting bugs in the network's new shielded pool.

The proof, written in Lean programming language, took three teams of researchers and cryptographers a month to complete and covers components needed for balance integrity, including Ironwood's zero-knowledge proof system, circuit rules, and ledger-level accounting.

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

The researchers said the new pool restores confidence in Zcash's supply integrity, and funds migrating from Orchard must pass through a public accounting checkpoint known as a turnstile, designed to prevent any hypothetical excess coins from entering Ironwood.