Zcash researchers published more than 2,700 machine-checked theorems to rule out undetectable counterfeiting bugs in Ironwood. Written in the Lean programming language, the proof required three teams of researchers and cryptographers over a month to complete. It establishes a security property known as balance integrity, ensuring the shielded pool cannot pay out more value than has publicly entered it. Ironwood was introduced in the NU6.3 upgrade in response to a vulnerability discovered in the Orchard shielded pool that could theoretically have enabled undetectable ZEC counterfeiting. Zcash developers found no evidence that the flaw had been exploited.
Source: Read the original article
