In this fireside chat, we invited Alexander Hicks, Researcher at Ethereum Foundation, to discuss about zkEVM Verification Project, which is an initiative under the Ethereum Foundation.

Alexander discusses his work on the zkEVM Verification Project, outlining key technical advances, the growing importance of zkVMs in Ethereum’s roadmap, and the security measures required to protect the next-generation L1 architecture.

Alexander and Kostas also discuss LLZK, an open-source intermediate representation (IR) for zero-knowledge circuits, developed by Veridise and supported by a grant from the Ethereum Foundation. Check out all the projects built on LLZK in our GitHub organization here.

The conversation was hosted by Kostas Ferles, CTO at Veridise, and filmed on 16th November 2025 in Buenos Aires.

See the full timestamps and text summary below.

Timestamps

00:00 Introduction
00:16 What are the main goals of the zkEVM Verification Project?
02:12 Current progress: what has been accomplished, what’s next?
20:57 Deep dive into LLZK: Current use cases. What developers are building now and in the future?
32:47 Where to learn more about LLZK projects and how to contribute?
34:20 The future of Ethereum, the EVM, and zkVMs: will users interact with zkVMs or L1 directly?
40:00 Could zkVMs eventually replace the EVM?
45:33 Closing remarks

Summary of the fireside chat

The fireside chat between Alexander Hicks (Researcher at the Ethereum Foundation) and Kostas Ferles (CTO at Veridise) provided a detailed look into the zkEVM Verification Initiative, focusing heavily on the foundational goals, technical progress, and Alexander Hicks’s personal predictions about securing the future of Ethereum L1.

Alexander asserts that zkVMs are critical to the future development of Ethereum’s L1, specifically as a scaling solution to move beyond the limitations of re-execution. He stressed that formal verification is not optional; it is a necessity to ensure Ethereum is not losing any robustness guarantees that people have come to expect from the layer 1. Due to the immense complexity of zkVMs, the risk of introducing a soundness bug that could lead to the worst case scenario of loss of funds, or a completeness bug causing a liveness issue, is too high to ignore. Hicks’s ultimate ambition is that formal verification will result in a system that is even more secure while also enabling improved performance and scalability for more users and even more transactions.

Confidence and concerns across key verification tracks

Alexander noted that progress across the initiative’s three tracks—zkVM circuits, the EVM guest program, and Cryptography—has been pretty good so far.

On the zkVM Track, Alexander expressed high confidence in the formal verification of RISC-V circuits against the rigorous Sail specification, which he finds promising. He reported significant efficiency gains: proofs that previously took months or cost several hundreds of thousands of dollars now require about ten weeks by one expert engineer. He is pretty confident this time could drop to a month or less soon.

Due to this success, Alexander expects that all of the zkVMs, which are candidates for the L1 should have the RISC-V circuits formally verified well ahead of mandatory proving.

However, Alexander admitted feeling conflicted about the growing reliance on pre-compiles. He stated it feels strange that we’re adding that many pre-compiles, viewing them as a bit like a performance bandaid and somewhat antithetical to the spirit of the zkVMs. To avoid the massive time sink of verifying potentially 60 to 100 manual pre-compiles forever, he is hopeful that the project can pivot to using compiler-verified auto pre-compiles.

The EVM Track aims to ensure guest programs (Ethereum clients like Reth) execute equivalently on RISC-V as they would on a formal EVM specification. While proofs show most EVM opcodes are equivalent, Alexander conceded that work remains, particularly regarding gas accounting, which he finds a bit of a mess to formalize, and then to go and verify. Furthermore, the lack of standardized RISC-V compile targets means different zkVMs produce different assembly code for the same client, which Alexander finds quite frustrating. He relies on the empirical robustness of SMT solver tools, offering a cautious fingers crossed for success.

The Cryptography Track tackles the gap between theoretical proof systems (like Plonky3s FRI) and their actual code implementation, a space that poses quite a bit of risk due to past critical bugs. The focus is on creating high-assurance, fully executable specifications in Lean to facilitate differential testing and ultimately verify the verifiers to ensure system-wide soundness.

The essential role of LLZK and compiler toolchains

Alexander expressed profound enthusiasm for LLZK (Low-Level ZK IR), noting he was very happy to see Veridise’s original proposal when Ethereum’s Verified zkEVM Project was started. He praised LLZK as a great example of trying to embed formal methods and formal verification into the development stack as a default. The ZK tools in AuditHub, a blockchain security platform developed by Veridise, run on LLZK.

Alexander champions the use of the underlying MLIR framework. He noted that MLIR’s use of dialects allows compilers to handle domain-specific optimizations (like replacing singular constraints with one high-degree algebraic constraint in KECCAK) which is crucial for maximizing performance gains. His personal opinion on the framework’s versatility and integrated assurance is that we should aim to implement everything in MLIR. He believes this approach provides better developer experience and performance than prior certified compilers like CompCert.

Ethereum’s long-term vision and architectural philosophy

Alexander is optimistic about the timeline: he is hopeful for optional proving on L1 by 2026 (after the Glamsterdam upgrade), leading to mandatory proving in 2027 or very early 2028.

Philosophically, Alexander said the verification effort is not purely ideological or out of fascination for verification. It has a productive goal to act as an accelerator, allowing the community to ship faster, secure code by removing reliance on time-consuming audits.

Regarding Ethereum’s future execution layer, Alexander believes zkVMs are going to change a lot. While the EVM must persist for backwards compatibility, zkVMs could enable developers to bypass the EVM entirely and write smart contracts in languages like Rust that compile directly to RISC-V.

Alexander offered his most compelling personal opinion on this subject: the actual key points are not necessarily like final ISA, of the zkVM, but rather the compiler toolchain. Focusing on infrastructure like MLIR, which can handle custom extensions and domain-specific optimizations, is more critical than debating the canonical Instruction Set Architecture (ISA). Ultimately, Alexander concluded that it is the community’s responsibility to have an informed discussion and illustrate what these trade offs are before committing to future architectural changes.