Zcash 形式化验证系列

一个由三部分组成的系列，从基本原理解释形式化验证，深入讲解 2026 年 Orchard 健全性漏洞，并展示 Ironwood 如何通过机器验证的数学证明予以回应。