根据 Project Tachyon 的说法，周二，Zcash 研究人员完成了对 Ironwood 的形式化验证，并发布了一份由机器检查的证明。该证明表明，在其所述的密码学假设下，该网络新的保密池不包含不可检测的仿冒漏洞。
该证明使用 Lean 编程语言编写，包含 2,700 多条定理，并在一个多月的时间里由三支研究人员和密码学家团队共同完成。该工作建立了余额完整性，确保保密池无法支付出超过其已公开进入的价值。该证明涵盖 Ironwood 的零知识证明系统、电路规则以及账本级别的核算，但不涉及隐私保证。
