Zcash researchers published more than 2,700 machine-checked theorems designed to rule out undetectable counterfeiting bugs in Ironwood. 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.