#formal-methods
6 posts tagged with “formal-methods”
If a compiler optimization is just runtime work you proved you don't have to do, why stop at machine code? Follow the thesis through the instruction set, the gates, the transistors, and off the digital cliff into analog and physics, and 'optimize the program' turns into 'find a physical system whose natural evolution is the program — and prove it.' This is the tower of interpreters, the verified spine that reaches down it, and the thermodynamic floor where it bottoms out.
- 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.
If you can prove that fast code means what the original meant, you decouple optimization power from optimization trust — and you turn every competitor's optimizer, every frontier LLM, into your improvement. This post takes the thesis from 'Prove More, Run Less' and asks the next question: where does that capability actually pay, who buys it, and what's the single cheap experiment that decides whether the whole thing is real?
An abstract interpreter is a proof machine — every sound invariant it computes constrains what the program can possibly do at runtime. Push that far enough and the analysis stops describing the program and starts compiling it. This is the precise sense in which 'the more you prove, the less you run,' why it is almost the same thing as 'compiling by proving,' and how a refinement relation you already have becomes a certifying optimizer for free.
Two tools is not a framework — it's two tools. What turns interpreters, abstract interpreters, symbolic executors, model checkers, type systems and provers into one bench is a shared substrate plus a six-slot instrument interface and one linking theorem per tool.
An interpreter, a compiler, an abstract interpreter, a symbolic executor and a theorem prover walk into a program. They each say something true; none contradict each other. Why that is a directed, earned relationship — not a freebie.