We Verified the Verifier: A First for Zero-Knowledge Proof Systems

Security

•

September 2, 2025

Summary

‍

Nethermind’s Formal Verification team worked with Matter Labs to prove the honesty of ZKsync’s on-chain zk-verifier. Using EasyCrypt, we completed the first-ever formal proof of this kind. This was done in a live zero-knowledge system, showing that hard formal methods have a place in the broader zk ecosystem.

‍

Read on to learn about the most important points, or visit the corresponding blog post for a full account of the effort. Most importantly, do get in touch to see how we can formally prove properties about your zk verifier.

‍

Background

‍

In recent years, zero-knowledge (zk) proofs have emerged as a transformative technology in bringing Ethereum closer to its goal of achieving scalability and privacy. The key to their usefulness lies in their ability to allow one party (the prover) to demonstrate succinctly to another party (the verifier) that a given statement holds.

‍

In the context of Ethereum, zk rollups leverage this ability and asymmetry by having:

‍

an off-chain zk prover, which is able to process a multitude of transactions and then generate a succinct proof that all these transactions were processed correctly according to some pre-defined rules; and
an on-chain zk verifier, which verifies the proofs provided by the zk prover, acting as a trustless arbiter of truth and ensuring validity of all rolled-up transactions.

‍

However, there are three main issues that could undermine the security of the system: incorrect zk circuits; malicious provers; and malicious verifiers.

‍

The Challenge

‍

While recognizing the importance of having correct zk circuits as well as the continuous and growing effort from the community that is going into their verification, we focus here on understanding the potential impact of the remaining two issues, as well as what it would mean to ensure correctness and security of the associated proof infrastructure components.

‍

On the one hand, if the verifier is honest but the prover is malicious, the worst-case scenario would involve liveness failures, but not safety failures. In particular, a malicious prover would not be able to generate a valid proof for an invalid computation, as the underlying cryptographic assumptions make this computationally infeasible. While liveness issues would admittedly be disruptive to the rollup operations, they could not, for example, result in funds being stolen or transactions being forged.

‍

On the other hand, a malicious verifier could accept invalid proofs (for example, those generated by a malicious prover) as valid, potentially leading to catastrophic security breaches of the rollup.

‍

Objectives

‍

Our goal was to ensure the correctness and security of critical proof infrastructure components, particularly in the face of potentially malicious provers and verifiers.

‍

Approach

‍

We set out to formalize and prove as many critical properties as possible using EasyCrypt. These properties include, for example: honesty, soundness, completeness, knowledge soundness, and zero-knowledge.

‍

Due to time constraints, we focused exclusively on verifying honesty, which ensures that the verifier implementation behaves exactly as specified. The work involved modeling, reasoning, and proof construction across multiple levels of abstraction.

‍

Tooling

‍

When it comes to the tooling, we opted for using the EasyCrypt verification tool. In particular, we extended EasyCrypt to support reasoning about Yul programs, as ZKsync’s verifier is written in Yul, and created the beginnings of a general infrastructure for verification of zk verifiers written in Yul.

‍

Results

‍

We have proven that the actual on-chain implementation of the ZKsync zk verifier in Yul is honest. Specifically, we used EasyCrypt to formally establish the correspondence between the implementation and an abstract model of an honest verifier. All of the technical details are available in the associated blog post. This effort took us roughly 2.5 months to execute, including the learning curve of EasyCrypt and the creation of the Yul model.

‍

Future Work

‍

While this project was scoped specifically to proving verifier honesty, we have also identified the next steps for broader formal assurance:

‍

Knowledge soundness: Existing pen-and-paper proofs cover a simplified version of the verifier, which could be adapted into EasyCrypt using prior work on Fiat-Shamir and Schnorr protocols.
Completeness: Achieving this would require modeling the honest prover in EasyCrypt to verify prover–verifier interaction.
Prover honesty: Currently out of reach, due to the prover’s size and complexity across multiple languages.

‍

Most importantly, and hopefully with backing from the Ethereum Foundation, we plan to build a verification infrastructure in the Lean proof assistant, that would allow us to make formal verification of zk verifiers the norm, rather than the exception.

^References:

^{[1] Mihir Bellare, Oded Goldreich.}^{On Defining Proofs of Knowledge}

^{[2] Denis Firsov, Dominique Unruh.}^{Zero-knowledge in EasyCrypt.}

^{[3] Thomas Attema, Ronald Cramer, and Lisa Kohl.}^{A Compressed Protocol Theory for Lattices.}

^{[4] Denis Firsov, Benjamin Livshits.}^{The Ouroboros of ZK: Why Verifying the Verifier Unlocks Longer-Term ZK Innovation.}

^{[5] Ariel Gabizon, Zachary J. Williamson, Oana Ciobotaru. PLONK:}^{Permutations over Lagrange-bases for Oecumenical Noninteractive arguments of Knowledge.}

^{[6] Ariel Gabizon, Zachary J. Williamson.}^{plookup: A simplified polynomial protocol for lookup tables.}