EthSystems 完成隐私池形式化验证，覆盖规范到 Sepolia 字节码
--
EthSystems 完成了对隐私池（shielded pool）的形式化验证，范围涵盖书面规范至 Sepolia 测试网字节码。验证过程使用 Lean、Halmos、Kontrol、Aeneas、Verus 等工具，并对验证器和部署进行逐字节重建核对。双花和价值守恒由 Lean 定理机器验证。验证中共发现 6 个问题，其中 3 个源于验证工具。团队列出哈希无碰撞、验证器拒绝伪造证明、合约行为与模型一致等剩余依赖假设。