ZK tool
Picus detects under-constrained bugs in your ZK circuits
Picus is a ZK tool developed by Veridise for detecting vulnerabilities in zero-knowledge circuits.
Purpose-built for ZK security, it automatically identifies under-constrained circuits before they reach production — helping teams achieve provable assurance.
Picus can also be used to formally verify that your circuits are free from under-constrained bugs.
What is Picus?
It’s an automated formal verifier that scans ZK circuits for constraint violations, especially under-constrained bugs, the most common and dangerous class of vulnerabilities in zero-knowledge applications.
Using symbolic inputs and constraint checks, Picus attempts to break your circuits and produce concrete examples of failure, giving developers actionable insights to fix them.
How does Picus work?
Picus uses a two-phase process—lightweight static analysis combined with deeper solver-based reasoning—to identify under-constrained circuits and generate actual input/output sets that break constraints.
Core features
Under-constrainedcircuit detection
Finds areas where constraints are too weak or incomplete, enabling false or exploitable proofs.
Concretecounterexamples
When a bug is found, Picus generates inputs that reproduce it — no guesswork required.
Formal assurance of determinism
Picus can also be used to prove that your circuits are free from under-constrained behavior.
Multi-languagesupport
Supports Circom and other DSLs; extensible to additional frameworks like Zirgen. More support coming with Veridise LLZK framework in the future.
AuditHubintegration
Use Picus during audits or in standalone workflows through Veridise’s AuditHub platform — making it an ideal ZK tool for audit readiness.
Use cases
Pre-auditcircuit validation
Identify critical issues early and streamline the external audit process.
Continuous verification
Ensure circuit integrity across code changes with seamless CI/CD integration.
Key tool in ZK security audits
A go-to ZK tool for ZK auditors: enhances audit depth and coverage.
Built for ZK security
ZK circuits are hard to test and easy to break. Research shows that over 96% of real-world ZK circuit-layer bugs come from under-constrained logic. Picus was designed to catch exactly these vulnerabilities, making it a must-have ZK tool for modern ZK development.
Why choose Picus?
Uncovers deep bugs that testing and type systems miss
Picus is formal verifier — you’ll get provable guarantees of circuit determinism
Generates reproducible counterexamples
Built for real-world ZK development workflows with CI/CD integration
Trusted ZK tool by leading ZK teams such as RISC Zero and Succinct
Discover what RISC Zero's CEO has to say about working with Veridise
Since 2024, Veridise has collaborated with RISC Zero, the team behind the RISC-V-based zkVM. While multiple audits were conducted, our work extended beyond point-in-time reviews.
Watch RISC Zero CEO Jeremy Bruestle share his experience working with Veridise, and his thoughts how we contribute to RISC Zero’s long-term security.
Case study: Provable ZK security for RISC Zero
By integrating Picus into their workflow, RISC Zero continuously detects critical under-constrained bugs as their code and circuits evolve — ensuring security guarantees stay intact. This approach saves time by eliminating the need to pause development for manual audits.
As RISC Zero writes, “ZK security isn’t just stronger — it’s provable.”
Try Picus today
Picus is available to Veridise audit clients through AuditHub. Whether you’re building a zkVM, a privacy-preserving app, or a custom proving system, this ZK tool helps you achieve provable ZK security from day one.
Interested in the standalone version? Get in touch — we’ll help you get set up.