Blanc proves properties of deployed Ethereum bytecode
In plain words
The paper introduces Blanc, a method for proving facts about the exact code running in an Ethereum contract. A helper proposes a readable map of the code, and Lean’s trusted checker compares that map with the deployed bytes before proofs use it.
The authors prove, among other results, that an Ethereum withdrawal-request contract’s end-of-block call succeeds and returns the oldest pending committed submissions in order, up to 16 per block. Each returned submission paid at least the fee computed by the bytecode, when the stated assumptions hold. The work covers eight deployed artifacts, not every contract.
The research
Can a contract’s proof still be trusted if its compiler changed what gets deployed? Ethereum nodes execute bytecode, and the 2023 Curve incident showed how a compiler defect could make a shared source-level lock behave differently in the deployed code. Source-only reasoning can miss that gap.
Blanc checks a structured reading of deployed bytecode against the actual bytes, then proves contract properties over an executable EVM model.
For the EIP-7002 withdrawal-request contract, they show its end-of-block call succeeds and returns the oldest pending committed requests in order, up to 16 per block. Each returned request comes from a committed submission that paid at least the fee computed by the bytecode. This holds under stated premises, and the bytecode-computed fee need not match the EIP fee.
The proofs depend on stated assumptions, and the paper has not checked the live storage needed to connect several older contracts’ theorems to their current mainnet states. Its eight artifacts demonstrate coverage, not that every contract can be verified.
Analysis
Deep
- Original paper authors
- Seulkee Baek
- Submitted to arXiv
- License
- arXiv non-exclusive