The AVAZAR (Automated Verification Tools for zkEVM Arithmetization) project aims at developing a suite of general-purpose tools for proving semantic equivalence of the arithmetization of a ZKVM, the input/output relation given by the witness computation code and the constraint system is the same. Our approach will rely on:
- Certified transformations from the witness computation code (in LLZK) to SMT formulas.
- Clustering techniques to improve scalability.
- SMT solvers capable of reasoning about polynomial equations over finite fields.
All this integrated in a general open source automated tool called AVAZAR.