Towards Formally Verified zkEVMs

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.

Speakers: Cody Gunton

Track: Applied Cryptography