README.md

Picus

Automated detection of under-constrained signals in zero-knowledge circuits

---

Picus is a security analysis tool for detecting under-constrained signals in zero-knowledge proof circuits. Given an R1CS constraint system, it verifies that all output signals are uniquely determined by the public inputs — or produces a concrete counter-example showing two distinct valid witnesses.

The techniques underlying Picus are described in the PLDI 2023 paper "Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs" (see Citation).

Looking for the original PLDI 2023 research artifact? See the artifact branch.

Prerequisites

Both z3 and cvc5 (with finite field support) are automatically compiled from source during cargo build. No manual solver installation is required.

Build dependencies: cmake, python3, python3-venv, C++ compiler (gcc or clang), make, bison, git, libclang-dev, pkg-config.

First build takes ~15-20 minutes (z3 + cvc5 compilation). Subsequent builds are incremental.

Faster builds with pre-installed solvers: If you already have solver libraries installed, you can skip compilation:

# Skip cvc5 compilation (requires cvc5 GPL build with CoCoA)
CVC5_LIB_DIR=/path/to/cvc5/lib cargo build --release

# Skip z3 compilation
Z3_LIBRARY_PATH_OVERRIDE=/path/to/z3/lib cargo build --release

For CVC5_LIB_DIR, headers should be at ../include/ relative to the lib directory (or set CVC5_INCLUDE_DIR separately).

Note on licensing: cvc5 is compiled with CoCoA (GPLv3) for finite field support. Picus source code is MIT-licensed. The compiled binary is a combined work under GPLv3 when distributed. See cvc5's COPYING for details.

Installation

# Option 1: Install to PATH
cargo install --path crates/picus-cli

# Option 2: Build and run locally
cargo build --release
./target/release/picus check --r1cs circuit.r1cs

# Option 3: Build and run in one step
cargo run --release -p picus-cli -- check --r1cs circuit.r1cs

# Option 4: Docker
docker build -t picus .
docker run --rm -v $(pwd):/data picus check --r1cs /data/circuit.r1cs

Use as a Rust Library

Picus can also be used as a library crate in other Rust projects:

[dependencies]
picus = { git = "https://github.com/chyanju/Picus", tag = "v1.7.0" }

use picus::{check_circuit, Config, CheckResult};

let result = check_circuit("circuit.r1cs", Config::default()).unwrap();
match result {
    CheckResult::Safe => println!("safe"),
    CheckResult::Unsafe { witness_1, witness_2 } => {
        // witness_1/witness_2: HashMap<String, BigUint>
        for (signal, value) in &witness_1 {
            println!("{} = {}", signal, value);
        }
    }
    CheckResult::Unknown => println!("unknown"),
}

See crates/picus/src/lib.rs for the full API, including check_r1cs_bytes(), check_r1cs(), and re-exported types.

Usage

picus check — verify circuit uniqueness

picus check --r1cs circuit.r1cs                              # default: cvc5 + ff
picus check --r1cs circuit.r1cs --solver z3 --theory nia     # z3 with integer arithmetic
picus check --r1cs circuit.r1cs --solver none                # propagation only
picus check --r1cs circuit.r1cs --lemmas all-bim             # all lemmas except bim
picus check --r1cs circuit.r1cs --format json                # JSON output
picus check --r1cs circuit.r1cs --dump-smt /tmp/smt/         # dump SMT queries

Flag	Default	Description
--r1cs <path>	required	R1CS binary file
--solver <cvc5|z3|none>	cvc5	Solver backend (none = propagation only)
--theory <ff|nia>	ff	Theory: ff (finite field) or nia (integer mod)
--timeout <ms>	5000	Per-query solver timeout
--selector <first|counter>	counter	Signal selection heuristic
--lemmas <spec>	all	Lemmas: all, none, all-X,Y (exclude), none+X,Y (include). Names: linear, binary01, basis2, aboz, bim
--format <human|json>	human	Output format
--dump-smt <dir>	—	Dump SMT-LIB queries to directory

Note: z3 + ff is not supported (z3 has no finite field theory). Picus will reject this combination.

picus info — inspect R1CS metadata

picus info --r1cs circuit.r1cs
picus info --r1cs circuit.r1cs --constraints

Documentation

Usage Guide	Result interpretation, solver differences, troubleshooting, large circuit strategies
Architecture	Crate structure, data flow, solver backends
Propagation Lemmas	Deduction rules and their implementation
Benchmarks	Test suite from real-world ZK projects
Future Work	Planned features and removed components
Changelog	Version history

Citation

@article{pailoor2023automated,
  author = {Pailoor, Shankara and Chen, Yanju and Wang, Franklyn and Rodr\'{i}guez, Clara and Van Geffen, Jacob and Morton, Jason and Chu, Michael and Gu, Brian and Feng, Yu and Dillig, Isil},
  title = {Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs},
  year = {2023},
  volume = {7},
  number = {PLDI},
  journal = {Proc. ACM Program. Lang.},
  articleno = {165},
  doi = {10.1145/3591283}
}

License

MIT