Zcash Completes Formal Verification of Ironwood, 2,700-Theorem Proof Rules Out Undetectable Counterfeiting

According to Project Tachyon, on Tuesday, Zcash researchers 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.

The proof, written in the Lean programming language, comprises over 2,700 theorems and was completed by three teams of researchers and cryptographers over the course of more than a month. The work establishes balance integrity, ensuring the shielded pool cannot pay out more value than has publicly entered it. The proof covers Ironwood's zero-knowledge proof system, circuit rules, and ledger-level accounting, though it does not address privacy guarantees.