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

吴说获悉，以太坊隐私基础设施研发公司 EthSystems 公布隐私资金池（Shielded Pool）形式化验证研究，验证范围从协议规范、零知识证明电路延伸至 Sepolia 测试网上部署的合约字节码。团队使用 Lean、Halmos、Kontrol、Aeneas 和 Verus 等工具，对防止双重支付、资产守恒、智能合约及钱包实现等进行多层验证。其中，防止双重支付和资产守恒已在 Lean 模型中获得机器验证。研究共发现 6 项问题，其中 3 项涉及验证工具本身，且其中 2 项可能导致工具错误地证明不成立的命题。EthSystems 表示，大部分证明由 AI Agent 编写，再由 Lean 内核逐一检查。