sorryfreeLast reviewed 2026-09-13
Index › Frameworks › Picus

Picus

Direct answerPicus 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
Repository
https://github.com/Veridise/Picus
Category
ZK circuit verification
Targets
CircomR1CSgnarkHalo2 (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 (2026-09-13)
Maintained; the Circom version is documented as legacy, LLZK-based Picus is current
First public release
2022

Last reviewed 2026-09-13 by the sorryfree editors.

What Picus does

The uniqueness property (sometimes called determinism or weak safety) is weaker than soundness: a circuit can be deterministic and still compute the wrong function. But it needs no specification, catches the dominant bug class, and finishes in minutes on many real circuits, which makes it the standard first pass in ZK audits.

Picus can return 'unknown' when the solver times out, and proving uniqueness of non-deterministic-by-design gadgets requires annotation. Veridise's LLZK IR extended it beyond Circom in 2026.

Where it is strong

  • 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 and caveats

  • Proves uniqueness, not functional correctness.
  • Timeouts and 'unknown' results on large circuits.
  • Cutting-edge features are in the commercial AuditHub version.

When to choose it

Run Picus on every Circom, gnark, Halo2 or Plonky3 circuit before an audit, and treat a clean result as necessary, not sufficient.

Who works with Picus

Veridise.

Top-listed for circuit verification work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website

Clean, sp1-lean, zkLean, Halva, LLZK, Garden, Lampe, proven-zk and gnark-lean-extractor, CIVER, Circomspect, zkFuzz, Coda, Ecne, NAVe, Verified Cairo AIR (Stone and S-two).

Sources

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt