@Zcash 的漏洞導致了 Ironwood，並對 Orchard 支付電路進行了形式化驗證。我熱愛並支持這項工作。 我也想強調，@Starknet 已經持續進行形式化驗證超過 5 年。 支持像 Zcash 這樣能迅速響應的優秀項目非常重要，就像這次的情況一樣。 同時，認可像 Starknet 這樣具有前瞻性、領先於行業的項目也至關重要。（詳情見下方文章） 我曾多次表示，Starknet 是那個已經擁有其他鏈聲稱「即將實現」的技術的系統。這一點在許多方面都已成真。 我們一直站在許多當時不被看好、但如今人人承認至關重要的選擇的最前線，包括後量子安全的 ZK-STARKs 作為最佳的擴容與隱私解決方案、輕量級 zkVM（Cairo 最佳）、Validium 數據可用性，以及形式化驗證。 形式化驗證意味著您使用如 Lean 系統這樣的自動化工具，以數學方式證明您的代碼是安全的。 要完全捕捉「代碼安全」的所有含義非常困難，但在我們的 CTO @LiorGoldberg2（Cairo zkVM 及語言的共同創建者）帶領下，我們已持續進行此工作超過 5 年。 最早關於 ZK 相關主張的形式化驗證論文（由 Professor Jeremy Avigad、Yoav Seginer 等人發表）證明了定義 Cairo VM 的多項式約束集是正確的。 如果您最近關注新聞，最近由 AI 發現並已修復的 Zcash 漏洞（另一個我共同創立、我極為自豪並支持的項目）涉及一個缺失的約束。 決定驗證其代碼以排除此類其他漏洞，是正確的一步。對 Cairo 核心 VM 進行此類驗證，使 StarkWare 團隊獲得了數學上的確定性：我們的 Cairo VM 中不存在任何缺失的約束。 因此，除了證明 Cairo 的核心 VM 外，我們還證明了 S-two STARK 系統（編譯器的一部分）以及許多標準 Cairo 函數庫中的功能。 工作完成了嗎？沒有。還有許多其他內容可以進行形式化證明。但我們致力於持續對所有與系統正確性與安全性相關的核心屬性進行形式化證明。看到其他項目也將形式化驗證視為重要工具，我感到非常欣慰。我為 StarkWare 在這方面走在前列而感到驕傲。這就是我們所理解的「面向未來的區塊鏈」。 想了解更多？ 以下詳細介紹了我們過去幾年在 Lean 證明方面的努力