Source-grounded architecture and Lean 4 proof planning for draft EIP-8282.
The analysis pins ethereum/sys-asm current main and the head of ethereum/EIPs PR 12057 as inspected on 2026-08-04. Read source pins and exact references first. Each flow keeps code behavior, EIP requirements, assumptions, and open specification differences separate.
- Open
diagram/index.htmldirectly. It is self-contained and works offline. - Read the flow target, artifact manifest, and proof plan.
- Run
npm ci && npm run export && npm run verifyto reproduce and validate browser exports.
No Lean theorem is claimed proved. The package identifies proposed relational statements, evidence, dependencies, and blockers.