How Veridise integrated AuditHub and Picus tool into RISC Zero’s development pipeline to catch ZK circuit vulnerabilities early.
RISC Zero is on a mission to make zero-knowledge computing mainstream. As the creators of a general-purpose zero-knowledge virtual machine (zkVM), RISC Zero is building foundational infrastructure for the future of privacy-preserving, decentralized applications. But with the power of zero-knowledge proofs comes the complexity of zero-knowledge circuit security—where one misstep can lead to subtle bugs and risk catastrophic exploits.
That’s where Veridise came in
In 2024, RISC Zero engaged Veridise to integrate AuditHub’s Picus—Veridise’s automated detection tool for underconstrained ZK circuits—into their development workflow. The goal? Ensure the integrity of the zkVM through provable and continuous verification of its core circuits.
The challenge: Proving the absence of ZK vulnerabilities, continuously
ZK circuit security is notoriously difficult to get right. Unlike traditional smart contract vulnerabilities, ZK-specific bugs often stem from underconstrained circuits—logic that technically satisfies the proof system, but for the wrong reasons. These flaws can bypass cryptographic checks or leak sensitive information without detection.
Underconstrained circuits accounted for 100% of the critical vulnerabilities we identified—4 out of 35 total findings.
RISC Zero’s zkVM—written in their custom ZK DSL, Zirgen—is a modular system, with numerous cryptographic accelerators and architecture-specific components. Prior manual audits offered only a snapshot in time. As the system evolved toward their next R0VM 2.0 release, the RISC Zero team wanted an automated, formal verification process that would run continuously, keeping pace with development and alerting them the moment a vulnerability was introduced.
Why AuditHub and Picus?
The solution: Picus & AuditHub integration
Veridise proposed an integrated solution built on two pillars:
- Picus would be used to automatically detect underconstrained logic in RISC Zero’s ZK circuits—particularly in their zkVM and its components such as the Keccak cryptographic accelerator.
- AuditHub was used to facilitate the audits. RISC Zero engineers collaborated with Veridise security analysts on issue status updates and managing the overall audit workflow.
From the beginning, the integration emphasized long-term collaboration. RISC Zero engineers worked closely with Veridise to adapt their ZK language constructs for Picus compatibility. The modularity of RISC Zero’s design—where each component could be reasoned about independently—proved instrumental in scaling the verification process.
Implementation highlights: Keccak & RISC-V circuits
The first major milestone was formal verification of the Keccak accelerator circuit—a critical component responsible for hashing within the zkVM. Picus was able to identify and prove the determinism and constraint completeness of this module.
Next came partial verification of the new RISC-V execution circuit—the heart of the zkVM’s general-purpose capabilities. Veridise used Picus to validate determinism across several instruction sets, confirming that the constraint system enforced correct execution paths and arithmetic behaviors. In total 35 issues were detected and mitigated.
All results were tracked within AuditHub, which provided real-time updates on what had been verified, what needed attention, and where regressions occurred as new code was introduced.
Screenshot from RISC Zero’s Github: Picus in action verifying Keccak module CI/CD integration
Impact: Continuous confidence in ZK security
Since integrating Picus and AuditHub, RISC Zero has seen a paradigm shift in how they manage ZK circuit security:
- Formal verification: RISC-V and the Keccak accelerator are now provably secure against underconstrained bugs.
- Continuous detection: New vulnerabilities introduced during future development are flagged early—before they hit production.
- Increased development speed: RISC Zero’s engineering team has increased development velocity without sacrificing assurance, thanks to automated checks embedded in the CI/CD pipeline.
- AuditHub transparency: Both RISC Zero’s internal security team and external auditors can now track verification results, and ensure accountability across the security lifecycle.
What’s next: LLZK integration and expanding power of AuditHub
To use AuditHub’s Picus, developers need to express their ZK circuits in an intermediate representation (IR) that Picus can understand. For most teams, this process is relatively straightforward—and the AuditHub team is available to assist with integration.
Looking ahead, AuditHub will support integration with LLZK, unlocking even more capabilities.
LLZK is a flexible framework inspired by LLVM, designed to unify diverse front-end languages and backend architectures. It improves both maintainability and security across the ZK ecosystem and serves as a foundation for seamless integration with a broader range of security tools beyond Picus.
In short, integrating with Picus is easy and delivers immediate value. Integrating with LLZK takes it a step further—opening access to an entire suite of current and future ZK security tools, including ZK Vanguard, and any additional solutions we build going forward.
ZK security that keeps up with innovation
With ZK systems becoming more critical to blockchain infrastructure, the need for continuous, verifiable security has never been greater.
While manual security audits remain essential for ZK projects, underconstrained circuits are the most common source of vulnerabilities. These issues are best addressed through automated determinism verification, which enables continuous assurance without compromising development speed or relying on repeated manual re-audits.
RISC Zero’s integration of Veridise tools has set a new bar for the industry—showing that determinism of the most advanced ZK systems can be proven not just in one point in time with manual audit, but forever, with the right combination of advanced ZK tools, automation, and ZK security expertise.
About AuditHub:
AuditHub is collaborative auditing platform, built for the unique needs of blockchain security teams. With integrated tooling, real-time tracking, and direct auditor-developer collaboration, AuditHub enables transparency and speed across the entire audit lifecycle.
About Picus:
Picus is the industry’s first automated detector for underconstrained circuits in zero-knowledge circuits. As part of AuditHub’s detection toolkit, Picus has uncovered critical ZK bugs in major protocols and is trusted by leading teams building the future of ZK solutions.
