Matter Labs and Nethermind just completed the first formal verification of ZKsync's on-chain zk-verifier. This is a major milestone for ZKsync and blockchain security!
The zk-verifier ensures that ZK rollups process transactions correctly. It checks the correctness of zero-knowledge proofs, which are central to making rollups scalable and efficient. If a verifier has errors, it could make the system vulnerable to attacks. But since verifiers are complex, ensuring their accuracy is no simple task, which is where we introduce Formal Verification.
Most rollups rely on human-conducted audits to catch errors. These audits can sometimes miss edge cases or subtle bugs in complex, low-level code like the zk-verifier. ZKsync, however, went beyond human-based audits by using formal verification—a mathematical approach that proves the correctness of the code. We described how the verifier should behave, using mathematical notation, and wrote a proof that the code matches this behavior. This is where computers step in. They can precisely and rigorously check code, making sure it's correct. We used this power to ensure the verifier’s logic is airtight.
Writing proofs in a way that computers understand was a huge task, made possible by skilled engineers and researchers. We used appropriate tools like EasyCrypt, a proof assistant, which helped speed up our progress. Formally verifying the zk-verifier gives the highest level of security assurance in any on-chain zk-verifier. This sets new standards for blockchain, influencing future developments in scaling and privacy solutions.
With decentralized systems growing fast, security and scalability are more critical than ever. This formal verification of ZKsync’s zk-verifier is a step toward building a more secure and scalable blockchain future. This announcement will be followed by a blog post and paper giving the details of this work, as well as an open-sourcing of the EasyCrypt proof that individuals can personally check.
We want to thank Denis Firsov, Nethermind, Julian Sutherland, and Igor Zhirkov for their contributions to this project!