How RISC Zero integrated AuditHub and Picus tool into its 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 integrated AuditHub’s Picus—an automated formal verifier for ZK circuits—into its development workflow. The goal was to ensure zkVM integrity through provable, continuous verification of 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—circuits whose constraints don’t uniquely determine all signals for a given public input. In practice, the circuit can admit multiple witnesses, so a malicious prover can choose a bogus witness that still satisfies the constraints and get a proof accepted. This breaks soundness (accepting false statements) and can lead to critical vulnerabilities.
In addition to the AuditHub and Picus integration, we also conducted a security audit. Underconstrained circuits accounted for 6 out of the 41 findings in the audit, and importantly 100% of the critical-severity vulnerabilities.
RISC Zero’s zkVM—written in their custom ZK DSL, Zirgen—is a modular system, with numerous cryptographic accelerators and architecture-specific components. 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
An integrated approach was adopted, 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 security audits. RISC Zero engineers collaborated with external 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 AuditHub’s engineers 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 verified the determinism of this module.
Next came partial verification of the new RISC-V execution circuit, the heart of the zkVM. Picus was used in external security audits to validate determinism across several instruction sets, confirming that the constraint system enforced correct execution paths and arithmetic behaviors. AuditHub’s Picus tool detected six underconstrained circuits, four of which were critical severity. The RISC Zero team resolved all of them, with fixes additionally confirmed in Picus. In total, 35 issues were detected and mitigated.
Picus 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
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: Once integrated into CI/CD, Picus automatically detects vulnerabilities before production. Continuous monitoring has caught bugs like this bug and this one during development, shifting from point-in-time audits to ongoing security assurance.
- 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 and collaboratio: Both RISC Zero’s internal security team and external auditors can track verification results through AuditHub, ensuring accountability across the security lifecycle.
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 verification, which provides strong guarantees of determinism that manual audits cannot match. Once set up, this continuous assurance runs automatically without requiring ongoing input from developers, enabling teams to maintain development speed without relying on repeated manual re-audits.
RISC Zero’s integration of AuditHub 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.