Picus: Automatic SMT-based underconstraint detection for Circom, R1CS, gnark and LLZK
================================================================================

Picus checks whether every output signal of a circuit is uniquely determined by its inputs, which is the automatic, specification-free way to detect underconstrained circuits. It runs on Circom, R1CS and gnark directly and on Halo2 and Plonky3 through LLZK, and Veridise has used it with LLZK to verify SP1 core operations and RISC Zero circuits.

Maintainer: Veridise
Website: https://github.com/Veridise/Picus
Category: ZK circuit verification
Targets: Circom, R1CS, gnark, Halo2 (via LLZK), Plonky3 (via LLZK)
Approach: SMT (cvc5, Z3 with finite-field theory) uniqueness checking; fully automatic, no proofs to write
Access: Open source (MIT); newer versions ship in Veridise AuditHub
Status: Maintained; the Circom version is documented as legacy, LLZK-based Picus is current
Strengths: No specification, no proof engineering, fast on small and medium circuits. | Broad frontend coverage through LLZK. | Widely used and cited; the reference tool for its property.
Limits: Proves uniqueness, not functional correctness. | Timeouts and 'unknown' results on large circuits. | Cutting-edge features are in the commercial AuditHub version.
Firms using it: Veridise
Sources: https://github.com/Veridise/Picus | https://veridise.com/blog/veridise-announcements/llzk-v1-0-a-new-phase-for-zk-shared-infrastructure/

Source page: https://sorryfree.com/frameworks/picus/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13