What is proved, what is checked, what is trusted.

EELS is the reference, not the Yellow Paper; the translation cites EELS by file and line. Every fork from Frontier to Osaka is a delta over its predecessor, Amsterdam is staged, and the OP Stack and Arc chain rules sit on top.

Emitters in Lean generate the ARM64 and x86-64 interpreters’ opcode handlers, the JIT’s chunk code, the gas formulas, the fork tables and the host’s effect layer — CALL, CREATE, SSTORE, SELFDESTRUCT, transaction application, fee settlement, block rewards. The effect layer is proved equal to each fork’s spec. A drift check requires the committed generated files to be byte-identical to what the emitters produce now, the effect proofs to check with no sorry, and no gas constant to be copied into the host by hand.

19 sorry remain in the spec layer — per-fork refinement theorems and three trie lemmas; none in an executable definition — and several forks’ refinement statements are still placeholders. A generated matrix lists every obligation and CI fails if the debt rises. The axiom closure of the audited theorems is checked against a committed baseline: Lean’s standard axioms only.

Gas used, logs bloom, receipts root, transactions root and withdrawals root are recomputed from the execution, and every sender is recovered from its signature. The header is checked against its parent by EELS validate_header — gas limit, base fee, blob gas, timestamp, number, extra data, difficulty — and the ommers by validate_ommers; the header rules are emitted from Lean too. Not checked: the proof-of-work seal (ethash).

On Ethereum every 10,000 blocks at the tip; on Arc at each anchor, every 32,768 blocks. A metric record carries the newest verified root, so you can tell whether a state root at or after its block has been checked. Between anchors, the header gate is the check.

The Cancun BlockchainTests (111,983 tests, Frontier to Cancun): 111,835 pass and none fail on both the threaded interpreter and the JIT; the 40 skipped and 108 expected failures are listed with their reasons. A sample runs in CI.

Blocks, transactions, logs, transfers, account and storage diffs go into a binary columnar log. Each sealed shard records a content hash over its canonical rows (independent of compression and grouping) and a digest of the file. The format is specified in Lean, where decoding is proved to invert encoding; the writer and readers are checked against vectors emitted from that spec, not proved equal to it. The fact log is hosted, not open source.

One pass over the rows, the same code for the history and the live tip. Each record carries its block, whether it is final, the metric’s version and the newest verified state root. Arc’s windows add their block range, the anchors checked in it, a sha256 over the sealed shard footers behind them, and an oracle check: USDC totalSupply() against the folded mints minus burns.