Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis

Shichen Huang, Zhenghe Jiang, Yi Jiang +3

Zero-Knowledge Ethereum Virtual Machines (zkEVMs) secure Ethereum rollups by generating zero-knowledge proofs that guarantee off-chain execution correctness. However, subtle implem…