Zcash 采用形式化验证以实现 Ironwood 升级

阅读时间 2 分钟

Zcash 开发者在 Orchard 保护池披露的会计缺陷暴露了传统审计的局限性后，转向对 Ironwood 网络升级进行形式化验证。该缺陷由 Shielded Labs 研究员 Taylor Hornby 发现并在已知被利用前修补。团队表示无法检测的伪造源于规范或密码学假设的缺陷，而非实现漏洞，并正在使用 Lean 定理证明器对 Ironwood 的密码学规范进行证明，贡献者来自 zkSecurity 与 Zcash 开放开发实验室。Ironwood 将关闭旧的保护池，发布修正后的替代池，并通过门闸迁移在 2026 年 7 月激活时展示供应完整性。

Ironwood 将通过形式化验证规范来防止无法检测的伪造。