We’re excited to announce that Veridise researchers had two papers accepted at CAV 2025 (Computer Aided Verification), one of the most prestigious conferences on formal methods. This marks an important milestone in our mission: strengthening the foundations of zero-knowledge (ZK) systems through cutting-edge research.
Why it matters
Zero-knowledge proofs are rapidly becoming the backbone of privacy-preserving and scalable blockchain systems. But building trustworthy ZK circuits is no easy task: small design errors can, and often do, lead to critical security vulnerabilities.
At Veridise, we believe rigorous, scalable verification is the key to securing this new frontier. That’s why our research team continues to push the boundaries of what’s possible.
Research highlights
🔹 Zequal: Verifying consistency in circuit templates
Zero-knowledge circuits are defined by two components: the constraint system (the equations that must be satisfied) and the witness generator (the logic that computes candidate solutions to those equations). Subtle mismatches between the two are one of the most common sources of security vulnerabilities, since they can allow invalid behavior to sneak through as “valid” proofs.
Zequal introduces a new method to formally prove consistency between these components across all circuit template instantiations. Unlike prior approaches, Zequal checks a stronger correctness condition, giving it the potential to catch more bugs that other tools would miss. This makes it an important step toward building ZK circuits that are not just functional, but provably robust against subtle design flaws.
🔹 Multimod: reasoning across multiple arithmetic domains
Real-world ZK applications often mix different kinds of arithmetic such as bitwise operations modulo 2ⁿ alongside field arithmetic modulo a large prime. These “mixed-modulus” constraint systems are notoriously difficult for existing solvers, which often time out when faced with the added complexity.
Multimod, a collaboration between Veridise researchers and colleagues at Stanford, introduces a novel solver architecture that partitions constraints by modulus, reasons within each domain independently, and then connects the results using algebraic lemmas. By handling a broader and more expressive class of modular constraints than prior techniques, Multimod has the potential to succeed where others stall, catching correctness issues in circuits that existing solvers cannot feasibly analyze. This makes it a powerful step toward scalable, automated verification of the arithmetic at the heart of modern ZK systems.
The bigger picture
The acceptance of two ZK-focused papers at CAV reflects a broader shift: the formal verification and cryptography communities are increasingly converging. As zero-knowledge systems move from research prototypes into real-world applications, the need for rigorous, scalable verification is becoming a shared priority. These papers are part of a growing body of work that connects long-standing ideas from program verification with the unique challenges of cryptographic proof systems and signals that the gap between these two fields is narrowing in exciting ways.
Looking ahead
As zero-knowledge adoption accelerates, so does the need for provably correct systems. These research advances show what’s possible, and Veridise is proud to be shaping the scientific foundations of this rapidly growing field.
If you’d like to dive deeper:
