Zcash завершил формальную верификацию Ironwood, выпустив доказательство исключения риска подделки ZEC с помощью теоремы Lean

Zcash 的 Tachyon 計畫於 7 月 29 日宣布，完成了對 Ironwood 屏蔽池的形式驗證，並發布了一項機器驗證證明，包含超過 2 700 個以 Lean 程式語言撰寫的定理。此次驗證建立了一種名為「餘額完整性」的安全屬性，有效排除在其既定密碼學假設下 Ironwood 存在無法偵測的偽造漏洞的可能性。

Tachyon 計畫的形式驗證完成：逾 2 700 個 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 供應完整性的信心。