EthSystems 用 AI 辅助验证以太坊隐私资金池，发现验证工具存在缺陷

EthSystems 公布以太坊隐私资金池形式化验证研究，范围覆盖协议规范、零知识证明电路及部署在 Sepolia 测试网的合约字节码。团队用 Lean、Halmos、Kontrol、Aeneas 和 Verus 等工具验证防双重支付与资产守恒，两项已在 Lean 模型中获机器验证。