Picus
Open SourceVeridise's automated verifier that detects under-constrained circuits by checking uniqueness of witness outputs.
About
Picus is a formal analysis tool from Veridise that automatically checks ZK circuits for under-constrained behavior by verifying that circuit outputs are uniquely determined by their inputs (the "uniqueness" property). It works on R1CS produced by circom and uses SMT solving plus domain-specific reasoning to either prove a circuit properly constrained or produce evidence of a soundness issue. Under-constrained circuits are the dominant ZK bug class, and Picus is one of the few tools that addresses them with formal guarantees rather than pattern matching. It grew out of academic research (the underlying technique was published at PLDI) and is maintained as open source by Veridise.