2026-11-05 –, Lotus Stage 2
zkEVM performance headlines arrive at an accelerating pace, but full and robust formal correctness guarantees have not yet been established for any zkEVM. We set out the properties that constitute a good specification, share what we learned by formally specifying the EVM state transition function in evm-sail, and describe progress toward verifying the safety of production zkEVM components.
In the zkEVM team at the Ethereum Foundation, we have been working in collaboration with the FV team to explore the application of formal methods to harden zkEVM's. In our presentation, we will cover our high-level methodology and then dive into several case studies on both formal specification and validation of zkEVMs. This will cover both the EVM state transition function and the zkVM's upon which it is executed. This matters now because zkEVMs are moving from research toward securing real value on L1. We will share what these techniques actually uncovered in production systems, and where the residual risk sits today. We hope that the audience should leave able to judge what a credible zkEVM correctness claim looks like, and what to ask of one.
Francesco Risitano is a research engineer working on Ethereum scalability and privacy. He has worked across the stack, including zkVM development at Polygon Miden, node client development at Scroll, and now at the Ethereum Foundation, where he works on Ethereum’s transition to execution proofs.
Research Engineer at Ethereum Foundation focused on ZKEVM-based scaling. Prev. proving systems engineering at Aztec, the private L2.