Zippel

Zippel is a choreographic language, compiler, and runtime for cryptographic proof systems. A single .zippel source file describes a protocol the way a cryptography paper would, and Zippel compiles it into a computation graph from which it derives:

• optimized, auto-parallelized prover and verifier binaries built on arkworks, and
• fully automated static analyses that check completeness and special soundness directly from the protocol's specification, using ideal membership over Gröbner bases.

Below is an example of Schnorr's ZKP written in Zippel:

proto schnorr<G: Group, F: Scalar<G>>(witness x: F, instance g: G, instance h: G) where h == g * x {
    let r = random<F>;
    u <- g * r;
    c <- challenge<F>;
    z <- r + x * c;
    verify(g * z == u + h * c)
}

We have implemented over 35 proof systems ranging from textbook Sigma protocols (Schnorr, Chaum-Pedersen) to modern SNARKs and polynomial commitment schemes (Groth16, Spartan, HyperPlonk, KZG, Bulletproofs, Hyrax, PST13, Dory).

They are available in examples/,

Status: research prototype. Zippel has not been independently audited. Do not use it to protect anything of value.

Quick start

Clone the repository and build it with Rust nightly; the exact toolchain is pinned in rust-toolchain.toml and resolved automatically by rustup. Zippel does not build on stable Rust.

git clone https://github.com/eniac/zippel
cd zippel
cargo build

The commands below use Cargo aliases defined in .cargo/config.toml, which work from anywhere inside the repository.

Running examples

cargo zrun run ipa                        # prove and verify at default sizes
cargo zrun run ipa --size S=10            # larger instance
cargo zrun analyze ipa --size S=1         # run registered analyses
cargo zrun analyze ipa completeness --size S=2 --backend singular
cargo zrun run --help                    # list examples
cargo zrunr run hyperplonk_piop --size S=3 # release mode

See examples/ for more protocols, or run cargo zrun run <example> --help for available options.

Typechecking a protocol

If you are developing a new Zippel protocol and just want to typecheck it to make sure your syntax is correct and there are no obvious bugs, you can use cargo zcheck. Note that typechecking does not invoke any of our static analyses. This only ensures the program is valid and the verifier is not using prover-only variables (instance, extra, random). Since Zippel has sized types, you can also specify the sizes. Some examples:

cargo zcheck examples/kzg/kzg.zippel
cargo zcheck --size N=2 examples/marlin_kzg/marlin_kzg.zippel

Pass --size NAME=VALUE for the sizes you care about; unset Size parameters default to the smallest values that satisfy size constraints and cover function overloads.

Formatting

cargo zfmt --check examples/*/*.zippel   # report unformatted files
cargo zfmt --write examples/kzg/kzg.zippel

Testing

cargo test

Some tests use the Singular backend (see Optional dependencies below) and are skipped with a warning when it isn't found on PATH.

Optional dependencies

Singular provides an alternative Gröbner-basis backend for the completeness and soundness analyses. It must be on PATH to be used.

Using Zippel as a library

See docs/library-usage.md for how to depend on Zippel from your own crate, then write, compile, run, and analyze a protocol.

Reading and citing our paper

Zippel will appear at S&P 2027. You can find our paper here. If you wish to cite our work, please use this:

@inproceedings{angel2027zippel,
  title        = {Zippel: A Language, Compiler, Runtime, and Analyzer for ZK Proof Systems},
  author       = {Sebastian Angel and Sydnie-Shea Cohen and Eleftherios Ioannidis and Pratyush Mishra and Alex Ozdemir and Yuxiang Qiu and Alireza Shirzad},
  booktitle    = {Proceedings of the IEEE Symposium on Security and Privacy (S\&P)},
  year         = {2027},
}

Reproducing our evaluation

artifact/ contains a Dockerfile and scripts that build Zippel and reproduce the benchmarks, completeness analyses, and special-soundness analyses reported in our IEEE S&P 2027 submission. See artifact/README.md for details.

Contributing

See CONTRIBUTING.md for development setup, the checks run in CI, and how to add a new protocol example.

License

Zippel is licensed under the MIT license.

Copyright (c) 2024-2026 University of Pennsylvania, Distributed Systems Lab.