ZecHub
پژوهش
کاوش در دانش صفر · حریم خصوصی · رمزنگاری
🔎
مجموعه راستیآزمایی صوری Zcash
مجموعهای سهبخشی که راستیآزمایی صوری را از اصول اولیه توضیح میدهد، باگ صحت Orchard در سال 2026 را مرور میکند و نشان میدهد Ironwood چگونه با یک اثبات ریاضی ماشینبررسیشده به آن پاسخ داد.
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.