Zcash developers are using formal verification to mathematically prove the correctness of the Ironwood network upgrade and shielded pool to rule out undetectable counterfeiting bugs after a recently disclosed vulnerability in Orchard exposed the limitations of relying on conventional code audits, as explained by developer and crypto researcher Sean Bowe in a Tuesday blog post.
Ironwood is designed to address a flaw discovered in the Orchard shielded pool and restore confidence in the cryptocurrency’s supply integrity. The flaw was discovered by Shielded Labs researcher Taylor Hornby and patched before any known exploitation.
According to the developers, undetectable counterfeiting can only arise from flaws in a protocol’s mathematical specification or from broken cryptographic assumptions, while implementation bugs always leave evidence that can be detected by replaying the blockchain with corrected software.
The team said its formal verification effort focuses on proving the correctness of Ironwood’s cryptographic specification rather than auditing implementation code, arguing this is sufficient to rule out undetectable counterfeiting bugs under standard cryptographic assumptions.
The work is being carried out with contributors from zkSecurity and the Zcash Open Development Lab using the Lean theorem prover alongside traditional audits and AI-assisted analysis.
