· ChainCatcher
EthSystems 完成隐私池形式化验证,覆盖规范到 Sepolia 字节码
以太坊机构隐私技术机构 EthSystems 宣布对其隐私池(shielded pool)完成了形式化验证,范围从书面规范一直到 Sepolia 测试网上运行的字节码。验证按层使用不同工具:模型、电路和哈希用 Lean,合约用 Halmos 和 Kontrol,钱包用 Aeneas 和 Verus,验证器和部署通过逐字节重建核对。 双花和价值守恒已由 Lean 定理机器验证。验证中共发现 6 个问…