Skip to content
热点事件持续更新

EthSystems完成隐私池形式化验证

2 篇报道2 个报道来源2 小时前更新

先了解这件事

AI 综述

以太坊隐私基础设施研发公司 EthSystems 公布其隐私池（shielded pool）的形式化验证研究，范围从协议规范、零知识证明电路延伸到部署在 Sepolia 测试网上的合约字节码。防止双重支付和资产守恒已在 Lean 模型中获得机器验证。 研究共发现 6 项问题，其中 3 项涉及验证工具本身，且其中 2 项可能导致工具错误地证明不成立的命题。EthSystems 表示，大部分证明由 AI Agent 编写，再由 Lean 内核逐一检查。 团队同时列出仍然依赖的假设：哈希无碰撞、验证器会拒绝伪造证明、合约行为与模型一致。

AI 根据报道生成 · 2 小时前更新

最新进展10月27日 20:43
EthSystems 用 AI 辅助验证以太坊隐私资金池，发现验证工具存在缺陷

报道时间线

沿着报道，了解事件的不同侧面。

10月27日
  1. 吴说区块链
    EthSystems 用 AI 辅助验证以太坊隐私资金池，发现验证工具存在缺陷

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

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

    以太坊机构隐私技术机构 EthSystems 宣布其隐私池（shielded pool）完成形式化验证，范围从书面规范一直到 Sepolia 测试网上运行的字节码。验证按层使用 Lean、Halmos、Kontrol、Aeneas 和 Verus 等工具，双花和价值守恒已由 Lean 定理机器验证。验证中共发现 6 个问题，其中 3 个出在验证工具本身。

本事件热度走势

还没有足够的连续观测数据，暂不绘制趋势。