ZecHub
Research
Exploring Zero-Knowledge · Privacy · Cryptography
🔎
Zcash Formal Verification Series
A three-part series that explains formal verification from first principles, walks through the 2026 Orchard soundness bug, and shows how Ironwood answered it with a machine-checked mathematical proof.
Formal VerificationOrchardIronwoodProtocol Security
Research
What Is Formal Verification?
Introduction to proving software correct instead of only testing it.
Research
The Orchard Bug: When a Proof System Has a Hole
Case study of the 2026 under-constrained Orchard circuit.
Research
Ironwood: Proving Money Cannot Be Faked
How Zcash answered the Orchard bug with a machine-checked proof.