EthSystems 完成隐私池形式化验证，覆盖规范到 Sepolia 字节码

以太坊机构隐私技术机构 EthSystems 宣布其隐私池（shielded pool）完成形式化验证，范围从书面规范一直到 Sepolia 测试网上运行的字节码。验证按层使用 Lean、Halmos、Kontrol、Aeneas 和 Verus 等工具，双花和价值守恒已由 Lean 定理机器验证。验证中共发现 6 个问题，其中 3 个出在验证工具本身。