Zcash 研究團隊完成 Ironwood 新隱私池的形式驗證，以 Lean 程式語言撰寫超過 2,700 個機器檢查定理，證明新池不存在不可察覺的假幣漏洞。
（前情提要：Zcash 升級 Ironwood 最新進度：多組織已達共識，形式驗證與審計同步推進）
（背景補充：Zcash 新節點客戶端 Zakura 上線：同步 5 倍速度、將 Visa 級 5 萬 TPS 是為長期目標）
Zcash 研究團隊完成 Ironwood 新隱私池的形式驗證，在週二發布了以 Project Tachyon 官方公告 為依據的機器檢查證明，確認新池在其聲稱的密碼學假設下不存在不可察覺的假幣漏洞。
2,700 定理堆砌出的數學保證
根據 Project Tachyon 的公告，這項證明使用 Lean 程式語言撰寫，包含超過 2,700 個定理，由三個研究團隊和密碼學家花費超過一個月完成。證明建立了一個稱為「平衡完整性」（balance integrity）的安全屬性，確保隱私池不會支付超過公共進入的價值。
研究人員表示，證明涵蓋了 Ironwood 的零知識證明系統、電路規則和帳本級別會計，但不包含 Ironwood 的獨立隱私保證。
從 Orchard 到 Ironwood：Zcash 的升級之路
Ironwood 是透過 Zcash 的 NU6.3 升級 引入的，目的是回應 Orchard 隱私池中發現的漏洞，該漏洞理論上可能導致無法察覺的 ZEC 假幣。Zcash 開發者表示目前沒有證據顯示漏洞被利用過。
從 Orchard 遷移到 Ironwood 的資金必須經過名為「旋轉門」（turnstile）的公共會計檢查點，設計上防止任何 hypothetical 多餘硬幣進入新池。隨著資金離開 Orchard，這個過程也能提供越來越多的證據，證明舊池是否曾被利用。
形式驗證的意義：比傳統審計更嚴謹
形式驗證（formal verification）與傳統程式碼審計不同，它不是靠人工檢查每一行程式碼，而是用數學定理證明程式碼在所有可能情況下都正確。Lean 程式語言是近年來形式驗證領域的熱門工具，已在多個密碼學專案中實證有效。
Zcash 此次的形式驗證工作涵蓋了 Ironwood 的核心元件，意味著新隱私池的「基礎會計」已經過數學保證，而非僅靠人工審計。這對於剛經歷過假幣漏洞事件的 Zcash 來說，是恢復市場信心的關鍵一步。
📍相關報導📍
Zcash 升級 Ironwood 最新進度：多組織已達共識，形式驗證與審計同步推進
Zcash 公開「Ironwood」提案：讓任何人都能驗證 ZEC 流通量，救得了信心？
Zcash 新節點客戶端 Zakura 上線：同步 5 倍速度、將 Visa 級 5 萬 TPS 是為長期目標
