# Audit of Zcash: Orchard

- **Client**: Tachyon Foundation
- **Date**: July 14th, 2026
- **Tags**: Halo2, Zero-Knowledge Proofs, Orchard, Zcash

## Introduction

On June 8th, 2026, zkSecurity started a security audit of the Zcash Orchard and Halo2 repositories on behalf of the Tachyon Foundation. The audit lasted one week with two consultants, and was a focused, high-priority review aimed at reducing tail risk in the Orchard and Halo2 code.

### Scope

The audit targeted the following release tags:

- The [orchard](https://github.com/zcash/orchard) crate at tag [`0.14.0`](https://github.com/zcash/orchard/tree/0.14.0).
- The [halo2](https://github.com/zcash/halo2) repository at tag [`halo2_gadgets-0.5.0`](https://github.com/zcash/halo2/tree/halo2_gadgets-0.5.0), covering the `halo2_gadgets`, `halo2_proofs`, and `halo2_poseidon` crates.

A primary focus was constraint soundness: the large Orchard Action circuit, together with the Halo2 gadgets it depends on. The review also covered the Halo2 proof system verifier and the non-circuit, verifier-facing surface of the Orchard crate. In concrete terms, the review spanned four areas:

- The **Orchard Action circuit** and its sub-circuits: note commitment (`NoteCommit`), incoming-viewing-key commitment (`CommitIvk`), value commitment, nullifier derivation, and Sinsemilla Merkle-path verification.
- The reusable **Halo2 gadgets** it builds on: the `halo2_gadgets` elliptic-curve, Sinsemilla, and utility gadgets, and the `halo2_poseidon` Poseidon circuits.
- The **`halo2_proofs` PLONK verifier**, transcript, and polynomial-commitment verification paths.
- The **Orchard crate's non-circuit surface**: bundle, action, and public-instance handling; value, nullifier, and note-commitment binding; key, signature, and address parsing; and the PCZT partial-transaction verification and extraction flow.

The Halo2 crates in scope also contain gadgets that Orchard does not use, most notably the SHA-256 circuit. At the client's direction, these components were excluded from the review. This report therefore makes no claim about their correctness; the SHA-256 gadgets are in fact known to contain serious soundness issues, outside the scope of this report.

Given the one-week timeframe relative to the size of the scope, the review was deliberately prioritized: effort was directed at the areas of highest risk and the most likely sources of soundness bugs, rather than at exhaustive, uniform coverage of every component. The findings in this report reflect the issues surfaced within that window, and the absence of findings in a given area should not be read as a guarantee that it is free of issues.

## Summary

A substantial part of the engagement went into an MVP formal verification of the entire Orchard Action circuit in Lean, built with [Clean](https://github.com/Verified-zkEVM/clean), zkSecurity's framework for formally verifying zero-knowledge circuits. This formalization, [described below](#formal-verification-of-the-orchard-action-circuit), is the most significant outcome of the audit: it gives us high confidence about circuit soundness against the [Zcash protocol spec](https://zips.z.cash/protocol/protocol.pdf).

The manual review and accompanying proofs of concept surfaced no issue affecting the security of the deployed Orchard protocol. The circuit-level findings concentrate on gadget-usage paths that are hard to maintain and dangerous to change, where a future modification could silently break a soundness assumption; rather than on live bugs in the current code.

[zkao](https://zkao.io), zkSecurity's AI security scanner for cryptographic code, was used during the engagement and flagged the empty-Sinsemilla and fixed-base-multiplication findings.

### A note on Halo2 gadget usage

Several observations during the review stem from general characteristics of the Halo2 constraint system rather than from defects specific to a single gadget. These four recur as footguns for anyone integrating the `halo2_gadgets` primitives:

- **Values are not cells.** A `Value<F>` passed into a gadget is used only during witness generation; it is never part of the constraint system. Unless the gadget copies it into an assigned cell and constrains that cell, nothing binds the value a caller supplies to the value the gates actually enforce. An honest prover always makes the two agree, so a missing binding is invisible on the happy path and only a malicious prover diverges.
- **Constraints apply only where the selector is enabled.** A gate constrains a row only when its selector is enabled on that row. Result cells written on rows where the selector is not enabled are assigned but unconstrained. A single missed enablement, for instance an off-by-one loop bound, silently leaves those cells free for a malicious prover to choose.
- **Semantically same cells are sometimes implicitly referred to by offset.** Similarly, a cell that's constrained on the chip configuration step is sometimes referred to in the synthesis step only by the documented offset. An offsetting error, such as an off-by-one, can miss those cells.
- **Risky APIs that are only used by tests are not gated.** Some APIs, such as `witness_decompose` are only used by tests. While their naming and usages are clear, they increase the risk surface.

The audited code uses the gadgets correctly.

### Formal verification of the Orchard Action circuit

To rule out correctness gaps in the Orchard circuits systematically, we formalized them in Clean, see https://github.com/zksecurity/clean-orchard. The work comes with end-to-end soundness and completeness proofs for the top-level Action circuit, covering all of its gadget dependencies. Proofs depend on zero sorries and a single benign axiom that establishes the Pallas curve order.

**Limitations**. The formalization was done within the circuit model of Clean, using raw constraints and a linear witness tape, which is a more primitive representation than Halo2 produces with its regions, custom gates and row-column layout. Because of that mismatch, an "approximate" rather than fully faithful style of porting circuits was chosen. The approach is [documented in detail](https://github.com/zksecurity/clean-orchard/blob/main/orchard-clean-plan.md) in the repository.

The main limitation, which follows from that approximation, is that our formalization **does not mechanically connect the ported circuits to their Rust source**, in any way. The translation of circuit code was done "by hand", in an AI-assisted manner, with strong instructions to use source-conformant circuits but no waterproof mechanism to enforce such conformance. Therefore, we could accidentally have formalized different circuits than Orchard actually uses.

A second limitation is that not all circuit specs and interfaces were human-written or reviewed, and such a review is essential for guaranteeing the proof gives us the properties we want. We did review and co-author the top-level Action circuit spec and have reasonable confidence of its appropiateness, but this does not rule out gaps in lower-level gadgets that the Action circuit does not happen to exercise.

As concrete evidence of how this can hide soundness bugs, consider [our finding](#finding-empty-sinsemilla-unconstrained-y) showing that the Sinsemilla hash circuit is unsound for empty input messages. The ported Clean circuit that LLMs produced works around this issue (which is standing in the way of the required `soundness` proof) by simply requiring the input message to be a [Vector of length `n + 1`](https://github.com/zksecurity/clean-orchard/blob/b5b93ee42a2b97ec2b997a4924c87c755663c5e8/Orchard/Sinsemilla/HashToPoint.lean#L1905-L1924). The Action circuit only uses inputs of length greater than zero.

Despite these limitations, we believe that the process we used would have exposed any end-to-end soundness gap with very high probability. As part of ongoing collaboration with Tachyon Foundation, zkSecurity is working on lifting both limitations, producing a circuit formalization that is mechanically checked to match the Halo2 constraint system, and where specs and circuit input signatures are carefully reviewed at each level.

<!-- TODO(gregor): write this section. Proposed structure:
  1. What it is — MVP formalization of the whole Orchard Action circuit in Lean using Clean
     (zkSecurity's ZK-circuit verification framework); machine-checked soundness + completeness.
     Link: https://github.com/Verified-zkEVM/clean/pull/402
  2. Why it matters — a proof that the constraint system enforces exactly the intended relation
     rules out entire classes of under-constraint bugs, rather than spot-checking. A primary audit
     output, complementary to the findings.
  3. Scope of the formalization — the full dependency stack (ECC; utilities; Poseidon Pow5/sponge/
     ConstantLength; Sinsemilla & Merkle depth-32; Orchard gadgets value_commit/derive_nullifier/
     spend-auth/note_commit/commit_ivk; top-level Action circuit wiring the 9 public-instance
     columns + q_orchard gate), ported source-conformantly against orchard-0.14.0 / halo2_gadgets-0.5.0.
  4. Method / modeling conventions — per-circuit semantic spec; custom gates -> FormalAssertion;
     copy constraints -> ===; Value<T> -> Unconstrained/UnconstrainedDep; verifier-fixed values ->
     Clean parameters/constants. Links: orchard-clean-plan.md, orchard-conformance-map.md.
  5. Status & limitations — MVP complete; top-level circuit assembled & proven sound+complete; no
     `sorry`s; rests on one axiom (pallas_natCard, the Pallas group order); top-level spec is
     currently an LLM-written IntermediateSpec, to be bridged to a hand-written Spec.
  6. Future work — path to a fully-specified proof (the Tachyon-funded Orchard formalization).
-->

## Findings

### Empty Sinsemilla hash leaves the output point's y-coordinate unconstrained

- **Severity**: Medium
- **Location**: sinsemilla/chip/hash_to_point.rs

**Description**. `hash_to_point` accepts a `Message` with zero pieces. The `Message` constructor only bounds the number of words from above, so an empty message passes:

```rust
fn from(pieces: Vec<MessagePiece<F, K>>) -> Self {
    // A message cannot contain more than `MAX_WORDS` words.
    assert!(pieces.iter().map(|piece| piece.num_words()).sum::<usize>() < MAX_WORDS);
    Message(pieces)
}
```

When there are no pieces, the hashing loop in `hash_all_pieces` never runs, so `hash_piece` is never called and no `q_sinsemilla1` row (nor the generator-table lookup or transition gate) is enabled. The returned y-coordinate is then assigned as plain advice into `lambda_1`, constrained only by the initialization gate:

```rust
// Hash each piece in the message.
for (idx, piece) in message.iter().enumerate() {
    let final_piece = idx == message.len() - 1;
    let (x, y, zs) = self.hash_piece(region, offset, piece, x_a, y_a, final_piece)?;
    offset += piece.num_words();
    x_a = x;
    y_a = y;
    zs_sum.push(zs);
}

// Assign the final y_a.
let y_a = {
    let y_a_cell =
        region.assign_advice(|| "y_a", config.double_and_add.lambda_1, offset, || y_a.0)?;
    // dummy lambda2 / x_p assigned as zero, since they are multiplied by zero
    y_a_cell
};
```

The initialization gate pins the output x-coordinate to `Q.x` and relates the y-coordinate only through a single equation:

```text
init_y_q_check:  2·y_Q − Y_A = 0,   Y_A = (λ₁ + λ₂)·(x_a − x_R),   x_R = λ₁² − x_a − x_p
```

Here `x_a` is fixed to the constant `x_Q` and `y_Q` to a fixed column, but `λ₁` (the returned y-coordinate), `λ₂`, and `x_p` are free advice.

A prover can pick any target `y` for the output and set the auxiliary cells `x_p = y² − 2·x_Q + 1` and `λ₂ = 2·y_Q − y`, which give `x_a − x_R = 1` and `Y_A = 2·y_Q`, satisfying the gate. We developed a proof-of-concept that drives a real `SinsemillaChip` on an empty message and returns `(x_Q, −y_Q) = −Q`, even though the specification defines `SinsemillaHashToPoint(D, []) = Q`.

**Impact**. This is an exploitable soundness gap for consumers of the Sinsemilla gadget that permit empty messages and use the returned point as a full curve point. It has no impact on Orchard, which does not hash empty Sinsemilla messages. Callers that only use the x-coordinate via `extract` are unaffected.

**Recommendation**. If empty messages are meant to be supported, constrain the empty case to return the domain point `Q = (x_Q, y_Q)`. The initialization already pins the returned x-coordinate to the constant `x_Q` (via `assign_advice_from_constant`); the empty branch should bind the returned y-coordinate to the constant `y_Q` in the same way, instead of assigning it as free advice. This fix lives entirely in the empty-message code path: it reuses the existing `fixed_y_q` and permutation machinery and adds no gate or column at `configure` time, so the constraint system that Orchard synthesizes is unchanged.

Alternatively, if empty messages need not be supported, reject them in `Message::from` / `Message::from_pieces` / `hash_all_pieces`.

### Full-width fixed-base multiplication does not bind the scalar to its window decomposition

- **Severity**: Low
- **Location**: ecc/chip/mul_fixed/full_width.rs

**Description**. Full-width fixed-base scalar multiplication decomposes a `ScalarFixed` into windows and computes `[windows]·B`, but it never constrains those windows to equal the witnessed scalar `value`. A `ScalarFixed` is created through the public constructor:

```rust
pub fn new(
    chip: EccChip,
    mut layouter: impl Layouter<pallas::Base>,
    value: Value<pallas::Scalar>,
) -> Result<Self, Error> {
    // ...
}
```

The `value` here is a host-side `Value`, used only during witness generation to derive the window assignments. Under the hood `new` calls `witness_scalar_fixed`, which ignores its layouter and assigns nothing, returning `EccScalarFixed { value, windows: None }`; the only cells are the window digits created later inside `.mul`, and they are range- and coordinate-checked only, never tied back to `value`. No equality constraint links the two. The relation the gadget actually enforces is therefore existential: `result = [windows]·B` for prover-chosen windows, i.e. "the output is `B` multiplied by some scalar the prover knows." It does not enforce that two multiplications sharing a single `ScalarFixed` object use the same scalar.

A caller who passes one `ScalarFixed` to two multiplications intending them to share an exponent gets no such guarantee. We developed a proof-of-concept that reuses a single `ScalarFixed` across `P = [α]·G` and `Q = [α]·H`, a discrete-log-equality (DLEQ) relationship. Because neither multiplication binds its windows to the scalar value, a prover can desynchronize them: the circuit accepts `P = [5]·G` and `Q = [11]·H` — two points that do not share a discrete log — even though a single `ScalarFixed` was passed to both.

This is an instance of a "value, not cell" gap: the API takes a `Value` and uses it to compute witnesses, while a caller might assume that passing the same value binds the two results to the same scalar. An honest prover always makes the windows agree with the value, so happy-path tests and witness-time self-checks pass; only a misuse combined with a malicious prover diverges.

**Impact**. The gadget is used correctly in the audited code. Orchard's spend-authority block reads as if it binds the scalar to a cell, but the same-scalar guarantee it visually suggests does not exist:

```rust
let alpha = ScalarFixed::new(ecc_chip, layouter.namespace(|| "alpha"), self.alpha)?;
let (alpha_commitment, _) = spend_auth_g.mul(layouter, alpha)?;   // [alpha]·SpendAuthG
```

Here `alpha` is a private prover hint, so the existential contract ("the output is the base multiplied by some scalar the prover knows") is exactly what Orchard needs, and no cross-multiplication scalar equality is relied upon. The issue is a latent footgun for other callers — such as a DLEQ construction — that would need two fixed-base multiplications to be pinned to the same scalar.

**Recommendation**. Document that full-width fixed-base multiplication enforces only an existential relation on the scalar and does not bind a reused `ScalarFixed` to a single value. Callers requiring a shared scalar across multiplications must bind it themselves — e.g. by copying the scalar cell into the running-sum decomposition (`copy_decompose`) rather than witnessing the windows from a `Value`.

### PCZT output verification does not authenticate the ciphertext against the approved note

- **Severity**: Low
- **Location**: pczt/verify.rs

**Description**. `Output::verify_note_commitment` reconstructs a note from the PCZT metadata (`recipient`, `value`, `rho`, `rseed`) and checks that its commitment equals the output's `cmx`:

```rust
let note = Note::from_parts(
    self.recipient.ok_or(VerifyError::MissingRecipient)?,
    self.value.ok_or(VerifyError::MissingValue)?,
    Rho::from_nf_old(spend.nullifier),
    self.rseed.ok_or(VerifyError::MissingRandomSeed)?,
)
.into_option()
.ok_or(VerifyError::InvalidOutputNote)?;

if ExtractedNoteCommitment::from(note.commitment()) == self.cmx {
    Ok(())
} else {
    Err(VerifyError::InvalidExtractedNoteCommitment)
}
```

This authenticates the note fields against the commitment, but it never inspects `self.encrypted_note` — the `enc_ciphertext` and `out_ciphertext`. Those ciphertext bytes are supplied by the PCZT constructor, and `tx_extractor.rs` copies them verbatim into the final action. Nothing in the verification helpers proves that the ciphertext actually encrypts the note whose fields the signer approves.

The `Output` documentation explicitly delegates this check to the signer ("The Signer can use `recipient` and `rseed` (if present) to verify that `enc_ciphertext` is correctly encrypted"), but the crate does not provide a helper that performs it. A signer relying on the available PCZT verification helpers therefore has no tooling to catch a malformed or mismatched ciphertext.

**Impact**. This is not a consensus issue — Orchard consensus does not require output ciphertexts to be decryptable. The impact is on signer/wallet flows: a signer can approve a semantically correct note (correct recipient, value, and memo per the metadata) while signing a transaction whose output ciphertext is undecryptable or encrypts different data. The recipient would be unable to detect or spend the note, effectively burning the funds, with no indication at approval time.

**Recommendation**. Provide a verification helper that checks `enc_ciphertext` (and `out_ciphertext`, when `ock` is available) against the approved note fields, and wire it into the documented signer checklist so that semantic approval covers the ciphertext the signer is committing to.

### Low-level proof verification accepts trailing bytes

- **Severity**: Informational
- **Location**: circuit.rs

**Description**. `Proof::verify` and `Proof::add_to_batch` feed the proof bytes into the Halo2 transcript without checking that the transcript consumes the entire slice:

```rust
let mut transcript = Blake2bRead::init(&self.0[..]);
plonk::verify_proof(&vk.params, &vk.vk, strategy, &instances, &mut transcript)
```

Halo2 reads exactly the expected proof elements and stops, so a proof carrying arbitrary trailing bytes is still accepted by these low-level APIs. Canonical size is only enforced elsewhere: `Bundle::try_from_parts` calls `validate_proof_size` when passed `ProofSizeEnforcement::Strict`, and PCZT extraction validates size before producing an authorized bundle. Consumers that call `Proof::verify` / `add_to_batch` directly, or construct bundles with `ProofSizeEnforcement::Unenforced`, get no such check.

**Recommendation**. Reject non-canonical proof length in the low-level verifier, or document `verify` / `add_to_batch` as transcript-only APIs that require a separate `Proof::expected_proof_size` check by the caller.

---

This report was published on the [zkSecurity Audit Reports](https://reports.zksecurity.xyz) site by [ZK Security](https://www.zksecurity.xyz), a leading security firm specialized in zero-knowledge proofs, MPC, FHE, and advanced cryptography. For the full list of audit reports, see [llms.txt](https://reports.zksecurity.xyz/llms.txt).