Zcash researchers have completed formal verification of Ironwood, publishing a machine-checked proof that the network\u2019s new shielded pool does not contain undetectable counterfeiting bugs under its stated cryptographic assumptions.\u00a0<\/p>\n
On Tuesday, Project Tachyon said<\/a> 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.<\/p>\n The researchers said the proof covers the components needed for that property, including Ironwood\u2019s zero-knowledge proof system, circuit rules and ledger-level accounting. It does not cover Ironwood\u2019s separate privacy guarantees.\u00a0<\/p>\n Ironwood was introduced through Zcash\u2019s NU6.3 upgrade<\/a> in response to a vulnerability discovered in its Orchard shielded pool that could theoretically have enabled undetectable ZEC counterfeiting<\/a>. Zcash developers said they found no evidence that the flaw had been exploited. The new pool was designed to restore confidence in Zcash\u2019s supply integrity.<\/p>\n 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.<\/p>\n Related: <\/strong><\/em>Why ZEC fell 40% even after Zcash patched a shielded pool bug<\/strong><\/em><\/a><\/p>\n