Seulkee Baek

Verifying deployed bytecode against executable EVM semantics, with exact gas and no added axioms

Much of Ethereum's most consequential code is immutable bytecode: old output of unverified compilers, and protocol logic run as contract code. We show that such bytecode can be verified as it is, without trusting what produced it, without simplifying the machine it runs on, and with no axioms beyond Lean's own. Blanc,...