ZK audits
Comprehensive ZK audit of your circuits and dapps to identify vulnerabilities and define recommendations on how to fix them.
We have experience with a wide range of zero-knowledge languages, frameworks and proving systems, including Circom, Halo2, Nova, Plonky2, gnark and others.
Trusted partner for several leading ZK projects
RISC Zero engaged Veridise for several ZK audits, including an audit of their entire zkVM. We integrated our ZK tools into RISC Zero’s CI/CD to continuously prove the determinism of their ZK circuits.
Linea engaged Veridise to audit their entire zkVM, which included an in-depth review of their 800 pages of documentation.
O1JS engaged Veridise to audit their ZK-DSL and CLI for deploying zero-knowledge apps on the Mina blockchain.
Semaphore engaged Veridise to audit their ZK protocol that allows casting a message (e.g. a vote/endorsement) as a provable group member without revealing your identity.
Jeremy Bruestle
CEO & Co-Founder of RISC Zero
Barron Caster
CEO & Co-founder at Demox Labs
Veridise has been incredibly helpful auditing all of our ZK technology, which requires deep domain expertise. We trust them, and have worked with them on a number of different projects—and will continue to.
Florian Kluge
Engineering Team Lead at o1Labs
Veridise did an excellent job auditing the o1js codebase. It’s not easy, given the complexity of the different programming languages, data flows, and how everything works together. Veridise really understands the internal workings. Amazing work!
Olivier Bégassat
Arithmetization Lead at Linea
I was surprised by the thoroughness of the audits and the really meticulous attention to detail. I initially thought the project would be impossible due to its size (800 pages of docs), and I’m really glad Veridise successfully completed it. It was a pleasure working with Veridise.
Uma Roy
Co-Founder and CEO of Succinct
We are super happy to have worked with Veridise. It’s clear they looked into our circuits in great detail. One of the bugs they found was critical and quite subtle, so we were impressed with their work.
Andy Guzman
Product Owner at Semaphore, Privacy & Scaling Explorations Team, Ethereum Foundation
The Veridise team was extremely detailed, helpful and collaborative during the audit and formal verification, it was a joy working with them.
Introduction to ZK audits
The Veridise difference: Why us?
Seasoned professionals
Veridise’s ZK audit team is composed of seasoned professionals with several PhDs in formal methods, software security and blockchain.
In-house tooling
In addition to rigorous human auditing, our in-house tools detect bugs that the human eye has a difficult time finding. This enhances the quality and effectiveness of our audits.
Confidentiality and ownership
We uphold the confidentiality of the report, although many of our clients find value in publishing it. Additionally, our reports become fully yours upon completion of the audit, unlike with some other providers.
Veridise’s edge: our in-house ZK audit tools
Veridise combines professionals who manually review code with our in-house tools.
Our in-house tools enable Veridise to detect hard-to-find bugs that are difficult for the human eye to identify, leading to comprehensive audit reports. With Veridise, your codebase is in the hands of industry-leading detection methods.
OrCa
Specification-guided fuzzer
Vanguard
Static analysis tool for smart contracts and ZK circuits
Picus
Zero-Knowledge Proof auditing tool finding bugs in arithmetic circuits
Special considerations with ZK audits
Auditing Zero Knowledge circuits and applications comes with unique challenges that Veridise is especially equipped to assess. We have detected a significant bug in all of our ZK audits.
Read more
Auditing Zero Knowledge circuits and applications comes with unique challenges that Veridise is especially equipped to assess. We have detected a significant bug in all of our ZK audits.
Traditional smart contract audits primarily focus on code correctness, vulnerability checks, and adherence to best practices, whereas ZKP audits also need to ensure the cryptographic elements function correctly without compromising privacy or security.
As an example, in ZK audits, auditors often need to validate the construction and evaluation of zero-knowledge circuits. Often this is checking underconstrained circuits, which means the circuit does not have enough constraints to uniquely determine all the variables in the computation. Multiple solutions may allow prover to create a seemingly valid proof for an incorrect statement, which may lead to serious vulnerabilities.
ZKP audits also often require the verification of the cryptographic primitives used, such as hash functions, commitment schemes, and elliptic curve operations, to ensure they are implemented securely and according to the specific requirements of the ZKP protocol.
Articles on Zero Knowledge
Veridise has developed industry-leading expertise in auditing Zero Knowledge Proof related applications. We have extensively written about Zero Knowledge related topics.
9 min read
Formal methods for ZK circuits at A16Z Crypto event
Watch this presentation by our President and Co-founder, Isil Dillig, detailing the evolution of our zero-knowledge security research and tooling.
Conference presentation on Zero-Knowledge
We’ve delivered presentation at numerous conferences about Zero-Knowledge and our in-house ZK vulnerability detection tools.
Formal methods for ZK circuits
54min | Isil Dillig | a16z crypto
Uncovering hidden security risks in ...
20min | Jon Stephens | Modular & L2 Day
Pushing the limits in the automated ..
71min | A. Bassa, D. Dominguez, J. Stephens
Lessons from the auditing trenches
15min | Kostas Ferles | L2con Brussels
Security in the ZK domains
19min | Alp Bassa | ZK Accelerate Athens
Practical security analysis of ZK ...
21min | Kostas Ferles | Carnegie Mellon University
Are your ZK Proofs Correct?
25min | Jon Stephens | Devcon Bogotá
Automatic detection of ZK Bugs
13min | Jon Stephens | IOSG OFP Denver
Zeroday: Why ZK Security is Important?
45min | Kostas Ferles | Nil Foundation
Picus: Push button ZK circuit verification
17min | Shankara Pailoor | EthCC 2023
Automated detection of ZKP vulnerabilities
16min | Alp Bassa | Secureum TrustX
Picus: Automated verification of ZKP...
15min | Andreea Buterchi | TrustX
Practical Security Analysis of ZKP...
21min | Kostas Ferles
Common Vulnerability Patterns in Aleo
29min | Jon Stephens and Kostas Ferles
ZK Circuits in dApps: Common Bugs to...
22min | Jon Stephens
Academic work on Zero-Knowledge security research
Certifying Zero-Knowledge Circuits with Refinement Types
Veridise ZK Team
IEEE Security & Privacy Conference
Oakland Security
Automated Detection of Under-constrained Circuits in Zero-Knowledge Proofs
Veridise ZK Team
Academic Paper
PLDI 2023
Practical Security Analysis of Zero-Knowledge Proof Circuits
Veridise ZK Team
USENIX Security Conference
Demystifying Loops in Smart Contracts
Veridise ZK team
CAV 2024
Computer Aided Verification conference
