EthSystems 完成隱私池形式化驗證，覆蓋規範到 Sepolia 字節碼

以太坊機構隱私技術機構 EthSystems 宣布對其隱私池（shielded pool）完成了形式化驗證，範圍從書面規範一直到 Sepolia 測試網上運行的位元碼。驗證按層使用不同工具：模型、电路和哈希用 Lean，合約用 Halmos 和 Kontrol，錢包用 Aeneas 和 Verus，驗證器和部署通過逐位元重建核對。

雙花和價值守恆已由 Lean 定理機器驗證。驗證中共發現 6 個問題，其中 3 個出在驗證工具本身。團隊同時列出了仍然依賴的假設：哈希無碰撞、驗證器會拒絕偽造證明、合約行為與模型一致。