All Posts

Published on
July 9, 2026
Formally Verified Autoprecompiles
powdr autoprecompiles are now e2e formally verified, using Lean.
Published on
July 3, 2026
yul-compiler: a formally verified Yul to EVM compiler, and the verified stack underneath it
yul-compiler is a work-in-progress formally verified compiler from Yul to EVM, built in Lean on top of two verified layers: yul-semantics and evm-semantics. We already have verified passes and a machine-checked correctness theorem.
Published on
March 17, 2026
powdr-wasm: an optimized zkVM for WebAssembly
powdr-wasm is an optimized zkVM for WebAssembly, built on top of OpenVM and the crush ISA.
Published on
September 22, 2025
Accelerating Ethereum with Autoprecompiles
In this article, we compare powdr's autoprecompiles to OpenVM's manually written precompiles and evaluate the technique on an Ethereum block verification benchmark.
Published on
May 21, 2025
powdr-OpenVM: end-to-end autoprecompiles
powdr and OpenVM are now integrated, supporting custom guest acceleration using autoprecompiles.