#lean
1 post tagged with “lean”
- Running an EVM Inside a Proof AssistantMay 27, 2026
Most EVMs you trust because they pass tests. This one you trust because the interpreter and its correctness proof are the same artifact, checked by a kernel you can't lie to. It executes real post-Cancun bytecode — decoder, stack machine, gas meter, fixture harness — and the same evaluator that runs your bytecode is the one a once-proved soundness theorem reasons about. Here's how that's possible, and why a single parametric `run` is the whole trick.