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.

Default builds are pure Rust: the in-tree native finite-field solver needs no external solver and no extra system dependencies. cvc5 / z3 are never compiled unless you opt in (see below).

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

# Or build and run locally
cargo build --release
./target/release/picus check --r1cs circuit.r1cs

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

The optional cvc5 and z3 backends are compiled only on explicit opt-in (--features cvc5 / z3) and carry extra build requirements (and, for cvc5, GPLv3 licensing) — see docs/building.md.

picus check --r1cs circuit.r1cs                   # verify uniqueness (native + ff)
picus check --r1cs circuit.r1cs --solver none     # propagation only, no solver
picus check --r1cs circuit.r1cs --lemmas all-bim  # tune propagation lemmas
picus check --r1cs circuit.r1cs --format json     # machine-readable output
picus check --r1cs circuit.r1cs --config my.toml  # load settings from a config file

picus info --r1cs circuit.r1cs --constraints      # inspect R1CS metadata

Configuration. No config is required — every setting has a built-in default. To customise, copy picus.default.toml (it documents every key), edit it, and pass it with --config <file>; or drop a ./picus.toml in the working directory and it is picked up automatically. Sources layer, with later winning: built-in defaults < config file < individual CLI flags. Full flag and configuration reference: docs/usage.md.

[dependencies]
# Tracks the main branch (the stable branch); default features = native
# solver only, no external build chain.
picus = { git = "https://github.com/chyanju/Picus", branch = "main" }

# To also build the cvc5 / z3 backends:
# picus = { git = "https://github.com/chyanju/Picus", branch = "main", features = ["cvc5"] }

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(), PicusConfig::from_file(), and re-exported types.

@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}
}

MIT