tzap 0.4.2

A super fast, Rust-based optimizer for large Clifford+T circuits

⚡️ tzap

A super fast, Rust-based optimizer for large Clifford+T circuits.

• tzap's philosophy is that each optimization pass should be linear in circuit size.
• tzap minimizes T-count with a new linear-time phase folding algorithm, based on this paper.
• tzap implements a new and fast superoptimization pass.
• The core optimization algorithms are fully formalized in Lean under formalization.

tzap is multiple orders of mangitude faster than other optimizers—and linearly scales to millions of gates!

Installation

Homebrew (macOS/Linux, easiest option):

brew install qqq-wisc/tap/tzap

pip / pipx (no Rust required, downloads a prebuilt binary):

pipx install tzap

crates.io (requires Rust; builds from source):

cargo install tzap-opt

From source (this repo, requires Rust):

cargo install --path .

Prebuilt binary (no Rust required, downloads and runs a shell installer) — macOS/Linux:

curl -LsSf https://github.com/qqq-wisc/tzap/releases/latest/download/tzap-opt-installer.sh | sh

CLI Usage

tzap also works as a Rust library; see the Rust API documentation.

Optimize a circuit

tzap input.qasm -o output.qasm

For example, using a benchmark in this repo:

tzap benchmarks/feynman/gf2^256_mult.qasm -o optimized.qasm

tzap output:

⚡️ tzap
  Parsing benchmarks/feynman/gf2^256_mult.qasm (13.9 MB)
	└─ 768 qubits · 1,115,899 gates · 393,981 2q gates · 458,752 T/Tdg · 10,711 depth · 1.530s

  Final result
	├─ Gates    1,115,899 → 657,723 (↓41.1%)
	├─ 2q gates   393,981 → 393,981 (↓0.0%)
	├─ T/Tdg      458,752 → 262,400 (↓42.8%)
	├─ Depth       10,711 →   8,162 (↓23.8%)
	└─ Time        3.104s

Optimization levels

Level	Description
-O1	Randomized phase folding + basic gate cancellation. Default.
-O2	Adds superoptimization to -O1.
-O3	Repeats -O2 until reaching a fixpoint.
-Osuper	Like -O3, but with more superoptimization power (slower on first use).

tzap -O3 benchmarks/feynman/gf2^256_mult.qasm -o optimized.qasm

Decompose Rz into Clifford+T

Use --decompose-rz when the target backend only accepts Clifford+T; tzap uses gridsynth. --epsilon trades approximation accuracy for circuit size (default 1e-10; larger is coarser).

tzap input.qasm -o output.qasm --decompose-rz --epsilon 1e-6

Use --decompose-cz to decompose CZ gates into H+CX+H before the optimization pipeline. With --passes, it is prepended to the listed passes.

Custom pipeline

--passes runs an explicit, ordered sequence of passes in place of the default pipeline.

tzap input.qasm -o output.qasm --passes CancelGates,PhaseFoldRand

Circuit support

tzap supports a subset of OpenQASM 2.0:

• Gates: h, x, z, s, sdg, t, tdg, rz, cx, ccx, ccz, cz, measure, reset
• Declarations: qreg, creg
• Not supported: classical conditionals (if), custom gate definitions (gate), barriers, include files (besides qelib1.inc, which is ignored)
• Unrecognized lines produce an error

Toffoli (ccx) and doubly controlled-Z (ccz) are auto-decomposed into Clifford+T. Controlled-Z (cz) is kept native so phase folding and cancellation can operate through it; use --decompose-cz for H+CX output. Rz is left as-is unless you pass --decompose-rz.

Correctness

1. Fuzzing and equivalence verification on small random circuits and benchmark circuits.
2. Lean formalization: core algorithms are implemented and proven sound in Lean 4 — see formalization.

Citation

If you use tzap in your research, please cite:

@misc{albarghouthi2026tzap,
      title={Linear-Time T-Gate Optimization via Random Abstraction}, 
      author={Aws Albarghouthi},
      year={2026},
      eprint={2605.13929},
      archivePrefix={arXiv},
      primaryClass={cs.PL},
      url={https://arxiv.org/abs/2605.13929}, 
}