Zcash 的 Tachyon 计畫於 7 月 29 日宣布，已完成对 Ironwood 屏蔽池的形式验证，并发布了一项机器验证证明，內容包含超过 2,700 个以 Lean 程式语言撰寫的定理。此次验证建立了一种名为「餘額完整性」的安全屬性，有效排除在其既定密碼学假设下 Ironwood 可能存在无法偵測的偽造漏洞的情況。
Tachyon 计畫的形式验证完成：逾 2700 个 Lean 定理
Tachyon 计畫的形式验证工作由三名研究人員与密碼学家团队合作完成，耗时一个多月；最終发布的机器验证证明包含超过 2,700 个定理，全部以 Lean 程式语言撰寫。此次验证的意義在於它是「机器验证」——即由计算机自动核查每一个逻辑步骤的正确性，而非僅依賴人工審阅，从而提供更高的確定性。
Tachyon 计畫表示，完成的验证在其既定密碼学假设下为 Ironwood 屏蔽池提供了不含无法偵測偽造漏洞的數学保证。
「餘額完整性」安全屬性：確保受保護资金池不超额支付的數学保证
「餘額完整性（Balance Integrity）」是此次形式验证所建立的核心安全屬性，其數学定義为：受保護的 Ironwood 资金池所支付的金额，不会超過其公开存入的金額。要实现这一屬性，验证工作所涵盖的組件如下：
· Ironwood 的零知識（ZK）证明系统
· 电路規則：構成 Ironwood 逻辑的基礎计算規則
· 帐本级会计：整个網路层面的资金追蹤与记账机制
值得注意的是，此次证明不涵蓋 Ironwood 的独立隐私保護措施；研究人員表示，隐私保障屬于独立的安全屬性，需要另外进行验证。
Orchard 漏洞的背景与「旋转閘门」的公开会计机制
Ironwood 屏蔽池推出的直接原因是 Orchard 安全池中被发现的漏洞——该漏洞理論上可能導致 ZEC 偽造行为无法被偵測，进而威胁 Zcash 的供应完整性。Zcash 在 NU6.3 版本升級中引入 Ironwood，开发人員表示尚未发现任何漏洞被实际利用的证據；新屏蔽池旨在恢复外界对 Zcash 供应完整性的信心。
从 Orchard 转移的资金必須通过名为「旋转閘门（Revolving Door）」的公开会计檢查点，目的是防止任何假想的超额代币进入 Ironwood；随着资金持续从 Orchard 流出，这一过程也可能逐步提供更多证据，用于评估旧资金池是否曾被濫用。
常见问題
Tachyon 计畫的 Ironwood 形式验证包含多少个定理，使用什麼工具完成？
根据 Tachyon 计畫的公告，此次形式验证包含超过 2,700 个定理，全部以 Lean 程式语言撰寫；由三名研究人員与密碼学家团队耗时一个多月完成；最終成果是一項机器验证的數学证明，由计算机自动核查每一个逻辑步骤。
「餘額完整性」安全屬性具體保证了什麼？
「餘額完整性」保证受保護的 Ironwood 资金池支付的金额不会超过其公开存入的金額；此次验证涵盖了实现这一屬性所需的所有組件，包括 Ironwood 的零知識证明系统、电路規則与帳本级会计；但此次验证不涵蓋 Ironwood 的独立隐私保護措施。
Zcash 为何需要引入 Ironwood，Orchard 漏洞是否已被利用？
Ironwood 是 Zcash 在 NU6.3 版本升級中引入的，旨在应对 Orchard 安全池中发现的一个漏洞——该漏洞理論上可能導致 ZEC 偽造行为无法被偵測；Zcash 开发人員表示，尚未发现任何该漏洞被实际利用的证據，新屏蔽池旨在恢复外界对 Zcash 供应完整性的信心。
