Proofs meet performance on the EVM

One picture: trust on one axis, speed on the other

Every approach to making the EVM faster makes a trade between how much you trust the result and how much speed you buy. Plotting them this way is clarifying — and it shows exactly the empty corner our work targets. Click a point.

Positions are qualitative. The diagonal from bottom-left (fast, untrusted) to top-right (proven, fast) is the field's frontier; the bottom-right corner — fast native execution with a machine-checked certificate — is largely empty, and is where a refinement-based checker would sit.

Compiling by Proving — when the proof is the optimization

The most striking recent paper, and the one closest to us. The traditional pipeline is "write a compiler, then (maybe) verify it." This inverts it: the act of proving a program correct produces the optimized code as a by-product, so optimizer and proof can never disagree — they're the same artifact.

The mechanism, intuitively

A K semantics is modular: one EVM opcode is many small rules. The paper builds an All-Path Reachability Proof (APRP) — a directed graph whose vertices are execution states and whose edges are steps (sequential), covers (subsumption), and branches (conditionals) — then compiles that graph back into code by step compression: adjacent edges vA →ᴹ vB →ᴺ vC collapse into one vA →ᴹ⁺ᴺ vC, erasing all the intermediate pattern-matching.

Their worked example is ADD. Executed modularly it fires five rules; compiled, those five become one:

What it actually buys (their numbers)

The scaling is the real message: opcode-granularity compilation gives consistent modest speedups; compiling whole programs by proof gives orders of magnitude — because the bigger the proven region, the more intermediate steps get compressed away.

Translation validation — let an unverified tool optimize, then check it

A different, very pragmatic philosophy from the Albert & Rubio group (Complutense Madrid et al., CAV 2023; extended 2025). Don't verify the optimizer — verify each optimization it produces. This is exactly the "untrusted search, verified certificate" split, and it's the strand most directly reusable by us.

The Coq framework has three pieces: a symbolic execution engine that runs a block to a symbolic state; a set of simplification lemmas that normalize symbolic states; and a checker that compares the two normalized states. If the optimized block's symbolic state matches the original's, the optimization is certified semantically equivalent — over all inputs, not sampled.

Limitation worth noting: it's confined to jump-free blocks — straight-line sequences, no control flow. Whole-program / cross-loop optimization is out of scope, which is exactly where an invariant-aware analysis (ours) could extend it.

SuperStack & friends — squeezing gas out of stack bytecode

These are the "untrusted search" half of the pattern above. They don't prove anything; they search for the cheapest equivalent instruction sequence and lean on a separate checker (or testing) for safety.

Key framing: these tools are where the cleverness lives — and precisely the part you do not want to formally verify, because the search heuristics churn constantly. The pattern says: let them be brilliant and untrusted; verify the artifact, not the engine.

revmc & native JIT — speed bought with a sandbox, not a proof

At the opposite extreme from "compiling by proving": compile EVM bytecode straight to native machine code for raw throughput, and get safety from isolation rather than correctness proof.

Our refinement machinery is a translation validator

The connecting insight: we built bN_refines / kevm_refines to prove our concrete interpreter ≈ KEVM. That is structurally identical to proving optimized block ≈ original block. The same observable-equivalence relation that powers Pillar B is a ready-made verified optimizer checker — and we'd be checking against a KEVM-faithful semantics, not a hand-rolled one.

Refinement-as-optimizer-checker, worked end to end

Here's how the B-track relation becomes a block-equivalence checker, with a real peephole rewrite and the negative test that makes it trustworthy. This reuses the exact shape of RefB7.lean — just block-to-block instead of step-to-KEVM.

-- the checker is just our observable-equivalence relation, block-to-block
def blockObs (ops : List Op) (c : Config) : Option (Obs Word) :=
  obsOf (EvmAlgebra.run aluConcrete (ops.length) (c.withCode ops))

def Optimizes (orig opt : List Op) : Prop :=
  ∀ c : Config, ObsRel (blockObs orig c) (blockObs opt c)   -- equal over ALL configs
                                                       -- (a gas-aware Obs adds: gas(opt) ≤ gas(orig))

...        ; stack top = x
PUSH1 0x00 ; stack: x, 0
ADD        ; stack: x+0 = x

...        ; stack top = x
(removed)
(removed)

theorem add_zero_optimizes : Optimizes [.push 0, .add] [] := by
  -- both leave the stack as `x :: rest`; ADD's denotation is `x + 0 = x` in Word
  intro c; simp [blockObs, EvmAlgebra.run, aluConcrete, Word.add_zero, ObsRel]
#print axioms add_zero_optimizes   -- ⊆ {propext, Classical.choice, Quot.sound} ⇒ certified

SWAP1  ; b, a, c
SWAP2  ; c, a, b   (NOT a permutation-identity)

(removed — wrongly treated as no-op)
(removed)          ; claims: a, b, c

-- the kill-#4-style negative test: the bad rewrite must FAIL to certify
theorem swap12_not_optimizable_to_nil :
    ¬ Optimizes [.swap 1, .swap 2] [] := by
  -- exhibit one config where observables differ: stack [a,b,c] with a≠c
  intro h
  have hbad := h (Config.ofStack [1, 2, 3])
  simp [blockObs, EvmAlgebra.run, aluConcrete, ObsRel] at hbad   ; [3,2,1] ≠ [1,2,3] ⇒ contradiction