Ethereum Foundation launches evm.fast challenge to verify block limits

An open challenge asks contributors to prove a finite worst-case step bound for Ethereum block verification on a RISC-V model The Ethereum Foundation has opened a technical challenge at evm.fast with an unusual target. The current best score is infinity. The task is to prove a worst-case limit on how much computation it takes to verify an Ethereum block. Any finite answer, backed by a machine-checked proof, beats the existing record. How the score works The challenge measures a number called K. K is the certified upper bound on execution steps for a 64-bit RISC-V model, applied to every input the challenge covers. Startup steps count toward the total, so contestants cannot quietly skip the warm-up. The model runs through Flapjack. Flapjack is a Lean 4 adaptation of the Pancake compiler, built for a 64-bit RISC-V architecture. Lean 4 is a proof assistant, software that checks mathematical proofs line by line. RISC-V is an open instruction set, the basic vocabulary a processor understands. The baseline program, compiled by the verified Flapjack compiler, already proves that block verification stops eventually. What it does not prove is a uniform bound, one fixed ceiling that holds ac...