Zcash researchers have completed formal verification of Ironwood, publishing a machine-checked proof that the network’s new shielded pool does not contain undetectable counterfeiting bugs under its stated cryptographic assumptions.
On Tuesday, Project Tachyon said that the proof, written in the Lean programming language, comprises over 2,700 theorems and took three teams of researchers and cryptographers over a month to complete. The work establishes a security property known as balance integrity, designed to ensure the shielded pool cannot pay out more value than has publicly entered it.
The researchers said the proof covers the components needed for that property, including Ironwood’s zero-knowledge proof system, circuit rules and ledger-level accounting. 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. Zcash developers said they found no evidence that the flaw had been exploited. The new pool was designed to restore confidence in Zcash’s supply integrity.
Funds migrating from Orchard must pass through a public accounting checkpoint known as a turnstile, which is designed to prevent any hypothetical excess coins from entering Ironwood. As funds leave Orchard, the process could also provide growing evidence about whether the old pool was exploited.
Related: Why ZEC fell 40% even after Zcash patched a shielded pool bug
