What does it mean to run an EVM 'inside a proof assistant'?	The interpreter is a total Lean 4 function — `EvmAlgebra.run` iterating a small-step `Config → StepResult Config`. Because it's a definition the kernel understands, you can both *execute* it on concrete bytecode and *prove theorems about it*. The artifact you run and the artifact you verify are literally the same code.
What is the one trick that makes the whole design work?	`run` is parametric. Instantiate it at the concrete state type `Config` and you get the EVM; instantiate it at an abstract domain (Sign, Interval) and you get a static analyzer — the *same* `run`. Soundness is then one theorem, `run_sound`, proved once by induction on fuel: if every opcode's per-step transfer is sound, the whole-program abstract run over-approximates the concrete run for all programs and all inputs.
Why is there no runtime 'congruence gate'?	An earlier design sampled abstract-vs-concrete agreement at runtime and hoped. That's gone. Now an unsound transfer function simply *fails to produce* the `SoundEvm` witness, and `lake build` goes red. A half-built or dishonest reading can't certify itself — it fails to compile a proof. The Lean kernel is the only trusted base.
Why keep a gas-free machine and a gas-metered machine separate?	Gas is an enforcement layer, not part of what a program *means*. The gas-free `aluEvm` is the soundness reference; the metered `aluEvmMetered` adds the opcode-cost frontier and out-of-gas halting and is proved to *refine* it. You get a clean theorem about computation and a clean theorem about resource bounds, with neither contaminating the other.