EIP-7002 提款合约在 Lean 4 中通过形式化验证
当前进展与背景
最新公开报道
最近报道 ·EIP-7002 合约在 Lean 4 中通过系统调用与 FIFO 性质形式化验证
作者 skbaek 在 Ethereum Research 发布研究提案，用 Lean 4 对 EIP-7002 提款请求合约的已部署字节码证明两条性质：系统调用总能成功且耗气不超过 210,000（上限 30,000,000），请求严格按先入先出顺序发出，提交、发出与剩余队列三列表恒等。证明基于 EVM 可执行语义 Jaune，覆盖 Prague、Osaka、BPO1、BPO2 四个分叉，仅使用 Lean 标准三条公理。作者同时给出反例：若系统地址存在代码，队列可被提前抽干；字节码按 256 位计算的费用可能低于 EIP 规定值（审计 Blackthorn L-8、Sigma Prime PEC-03 已标记溢出），机器检查的合成历史证明该保证不成立，但均非规范部署起点，也未证明主网可达。相关论文 arXiv:2610.19764v1 覆盖八个已部署产物，本帖仅聚焦 EIP-7002。
Ethereum Research · 社区研究提案 · 查看报道与出处 →报道时间不等于事件生效时间；具体状态与适用对象请对照来源。
背景综述 · AI 整理
以下帮助了解背景；涉及安排、版本或状态时，以较新的具体报道为线索核对。
作者 skbaek 在 Ethereum Research 发布研究提案，用 Lean 4 对 EIP-7002 提款请求合约的已部署字节码证明两条性质：系统调用总能成功且耗气不超过 210,000（上限 30,000,000），请求严格按先入先出顺序发出，提交、发出与剩余队列三列表恒等。证明基于 EVM 可执行语义 Jaune，覆盖 Prague、Osaka、BPO1、BPO2 四个分叉，仅使用 Lean 标准三条公理。作者同时给出反例：若系统地址存在代码，队列可被提前抽干；字节码按 256 位计算的费用可能低于 EIP 规定值，但均非规范部署起点，也未证明主网可达。
综述整理于
报道时间线
沿着报道，了解事件的不同侧面。
- Ethereum Research · 社区研究提案EIP-7002 合约在 Lean 4 中通过系统调用与 FIFO 性质形式化验证
作者 skbaek 在 Ethereum Research 发布研究提案，用 Lean 4 对 EIP-7002 提款请求合约的已部署字节码证明两条性质：系统调用总能成功且耗气不超过 210,000（上限 30,000,000），请求严格按先入先出顺序发出，提交、发出与剩余队列三列表恒等。证明基于 EVM 可执行语义 Jaune，覆盖 Prague、Osaka、BPO1、BPO2 四个分叉，仅使用 Lean 标准三条公理。作者同时给出反例：若系统地址存在代码，队列可被提前抽干；字节码按 256 位计算的费用可能低于 EIP 规定值（审计 Blackthorn L-8、Sigma Prime PEC-03 已标记溢出），机器检查的合成历史证明该保证不成立，但均非规范部署起点，也未证明主网可达。相关论文 arXiv:2610.19764v1 覆盖八个已部署产物，本帖仅聚焦 EIP-7002。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。