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

以太坊机构隐私技术机构 EthSystems 宣布，其隐私池已完成从书面规范到 Sepolia 测试网运行字节码的形式化验证，双花和价值守恒已由 Lean 定理机器验证。验证按层使用 Lean、Halmos、Kontrol、Aeneas 和 Verus 等工具，共发现 6 个问题，其中 3 个出在验证工具本身。团队同时列出仍依赖的假设：哈希无碰撞、验证器会拒绝伪造证明、合约行为与模型一致。