#programming
6 posts tagged with “programming”
- 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.
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.
Most of what engineers do is a substitute for a proof they don't have. Here's the thesis, the 50-year research tradition behind it, and the first vertical where the gap is unconscionable.
- Lattice Algebra in KindScriptFeb 16, 2026
Understanding the mathematical foundations of architectural enforcement through interactive visualizations.