Formal Verification of Zcash Ironwood Completed

Ironwood is a new shielded pool activating in Zcash today as part of NU6.3. In our last post, we showed how formal verification can eliminate the possibility of undetectable counterfeiting bugs. Bugs of this kind only exist in the protocol's specification, which is ideally suited to formal analysis.

Today we are publishing a machine-checked proof, written in Lean, which shows that undetectable counterfeiting bugs do not exist in Ironwood. The proof is publicly available in the ironwood repository and comprises more than 2,700 theorems. It took three teams of researchers and cryptographers well over a month to complete.

All of this work culminates in a single security property called balance integrity.¹ The vast majority of our effort was spent proving knowledge soundness for Ironwood's zk-SNARK, which is the primary focus of this post. But balance integrity depends on several other components of the protocol as well, and our proof addresses each of them, down to named assumptions.

Knowledge Soundness

zk-SNARKs are used in Zcash to let users demonstrate that they possess hidden transaction data that satisfies certain rules. That transaction information is encoded into a witness for some relation representing those rules, and the SNARK itself is a short argument that the prover knows such a witness. The verifier ingests the proof string, performs a computation, and then accepts or rejects.

Ordinary soundness is insufficient for shielded protocols; because a hidden transaction can contain anything, essentially every instance admits a witness.² Knowledge soundness is stronger, requiring the prover to actually know a satisfying witness. We show this using a notion in the style of Bellare–Goldreich: an extractor with black-box access to the prover must be able to produce a witness whenever the prover convinces the verifier.³

Schnorr proofs don't reveal to the verifier; that's one of the points of the scheme. But suppose the prover can be rewound to the moment just after it sent , and challenged again with a different . If it answers with a valid for the same , the two verification equations subtract to , and so , exactly the witness the extractor must produce.

This is special soundness: a witness can be computed from enough accepting transcripts at distinct challenges, and knowledge soundness follows. Public-coin protocols, in which the verifier only sends random challenges, are often proven knowledge sound this way. The technique generalizes to multi-round protocols like ours, where the accepting transcripts form a tree with a fork at every challenge round.⁴

However, protocols built using the inner product argument, including ours, typically suffer large extractor runtimes from traditional special soundness analysis, since filling the tree takes a number of accepting runs exponential in the round count. This doesn't lead to a concrete break, and many protocols ignore it in practice, but an extractor this expensive cannot support a concrete security claim: at our depth, extraction can cost more than attacking the discrete logarithm outright.⁵

Algebraic Provers

Our analysis instead models the prover as algebraic⁶, meaning that for every group element it emits, it must also expose a representation over the generators it has seen.

Schnorr provers in this model now expose with when they emit . The extractor substitutes that representation into the verification equation , rearranges to , and computes . No rewinding happened: the witness came out of a single accepting run. Extraction fails only at , one challenge out of , and was already fixed when arrived. Failures of this kind are charged to the knowledge error, the threshold that a prover's success probability must exceed before extraction is guaranteed.

That is the shape of our entire analysis. In Ironwood, the prover's representations are written over the URS⁷ (in our Lean code, AlgebraicProofString), whose generators are themselves derived by hash-to-curve; the URS is a trustless setup that anyone can recompute.⁸ Because every commitment in a proof arrives with a representation, the extractor always holds a candidate witness, and the work is in proving that a wrong candidate cannot survive verification. Each way it could is either accounted for exactly, like above, or converted into a computed break of a hardness assumption.

Extraction here means recovering openings of the commitments in a proof, and nothing about a commitment alone makes its opening unique. The security claim is that no efficient adversary can find a second one. Any ambiguity in extraction directly yields a nontrivial discrete-log relation among the URS generators:⁹

-- A concrete break: a nontrivial relation among the generators.
structure NontrivialDLRelation (urs : URS G) where
  coeffs : Fin (2 ^ urs.k) → F
  nontrivial : coeffs ≠ 0
  relation : commitGen urs.g coeffs = 0

-- Two distinct openings of one commitment yield such a relation.
def NontrivialDLRelation.ofCollision (urs : URS G) {a a' : Fin (2 ^ urs.k) → F}
    (hcol : commit urs a = commit urs a') (hne : a ≠ a') :
    NontrivialDLRelation urs

Relations of this kind always exist. The hardness assumption forbids computing one, which is why the break is data rather than a bare existence claim. Because an algebraic prover must write each point as a combination of the generators, a binding collision anywhere in the construction reveals such a relation, and the reduction turns it into an ordinary discrete logarithm.

Fiat-Shamir Transformation

As with Schnorr signatures, our protocol is made non-interactive with the Fiat-Shamir transformation in the random oracle model.¹⁰ In the deployed protocol, each challenge is "squeezed" out of a hash of the transcript so far, representing the oracle's response to the current prefix of the transcript.¹¹ This allows us to analyze the non-interactive verifier through the lens of its underlying interactive protocol. In our Lean code, the squeeze function is the oracle itself:

-- Use the random oracle as the Fiat-Shamir squeeze function.
def roChallenges O init proof :=
  deriveChallenges (ofOracle O) init proof

Non-interactivity lets a cheating prover grind for favorable verifier challenges, varying its own transcript and querying the oracle repeatedly. Our analysis measures this power with a parameter , the number of queries the adversary may make to this oracle.¹² Each query at a new prefix hands the prover another fresh draw, but by the time a draw arrives, its prefix is already fixed, and so is everything the extractor will read from that prefix.

Inner Product Arguments (Bulletproofs)

Ironwood's polynomial commitment scheme is built from an inner product argument (IPA). In each round of the IPA, the prover sends two round commitments, and the verifier's challenge folds the two halves of a witness vector; where Schnorr has a single challenge round, the deployed IPA has eleven, taking the vector down to one scalar.

Because the prover is algebraic, each of those commitments arrives with a representation, so the extractor holds a candidate opening at every stage of the fold. It remains to prove that a wrong candidate cannot survive the rounds. We follow the discrepancy between the prover's claim and its own representations as the rounds fold:¹³

-- Advance the claimed-opening discrepancy through one IPA round.
def ipaDiscrepancyStep (current : Fp) (round : Fp × Fp) (challenge : Fp) : Fp :=
  current + challenge⁻¹ * round.1 + challenge * round.2

-- The quadratic whose roots record a nonzero discrepancy becoming zero.
def ipaDiscrepancyPolynomial (current : Fp) (round : Fp × Fp) : Polynomial Fp :=
  C round.1 + C current * X + C round.2 * X ^ 2

-- A nonzero-to-zero transition means the challenge hit one of its roots.
theorem ipaDiscrepancyStep_mem_badSet (round) (h : current ≠ 0)
    (hstep : ipaDiscrepancyStep current round challenge = 0) :
    challenge ∈ szBadSet (ipaDiscrepancyPolynomial current round)

A wrong candidate can survive verification in only two ways. If the discrepancy ends nonzero, the extractor holds two different openings of one commitment, the computed discrete-log relation from before. If it returns to zero, some round's challenge landed on a root of its quadratic, a polynomial fixed before the challenge was squeezed: two roots per round, eleven rounds, and grinding attempts add up to , the first term of the bound we display below. If neither happens, the candidate is the witness.

Every other statistical term arises the same way: a set of roots pinned before its challenge was squeezed, counted once per oracle query.¹⁴ The multiopen argument and the quotient check contribute their own families, and one more challenge has a single excluded value (, where is the challenge that binds the claimed value into the IPA opening). None of them ever needs the prover to run twice.

The Concrete Reduction

The random oracle ensures that each of the polynomials above is fixed before its challenge is drawn, the algebraic model turns any ambiguity in extraction into a computed discrete-log relation, and the DLOG assumption forbids computing one. Because everything between the assumptions is machine-checked, the reductions compose into a single chain from a convincing prover down to a discrete logarithm.

Following that chain end to end gives the security claim: the probability that the verifier accepts while the extractor comes up empty is at most the advantage of a derived DLOG adversary, plus error terms. The traditional move at this point is to argue that every loss is polynomially bounded and leave it at that. We instead prove a concrete bound for the deployed protocol, making every loss explicit.

For the curves and fields Ironwood deploys, the labeled terms are negligible at any feasible query budget: even oracle queries at leave their sum near .¹⁵ The burden falls on 's advantage alone. A prover whose success against the extractor exceeds those terms hands over, as computed data, an algorithm for DLOG.¹⁶ The best known attack on DLOG over Vesta is Pollard's rho, at roughly group operations. Ironwood's zk-SNARK is therefore knowledge sound.¹⁷

The Verifier Fingerprint

The zk-SNARK verifier written in Rust and used by Ironwood can be thought of as a function that takes a proof string and public instance as inputs and returns a decision bit (accept or reject) as output. We can prove that some formalized protocol has knowledge soundness, but it would mean nothing if we did not show that it is faithful to the real verifier.

We are fortunate that the real verifier is more structured than a bare decision bit. In fact, it returns the coefficients of a linear combination of group elements (a multi-scalar multiplication, or MSM) derived from the proof string, the public instance, the verifying key, and the URS. The consensus rules then evaluate this combination and accept the proof only if the result is the group identity.¹⁸ Every coefficient is determined by the transcript, so each proof has exactly one canonical combination, computable by anyone from public data.

There is thus a single symbolic combination, with the proof string and instance left as variables, that describes how those coefficients are computed. We call this symbolic combination the verifier's fingerprint, and it is where we draw the boundary between mathematics and software:

• Above the boundary, our Lean proofs define the verifier to be the fingerprint, and the entire knowledge soundness analysis rests on exactly that object. We can think of the real verifier as any black box that reproduces its output.
• Beneath the boundary, the Rust code that assembles and evaluates the combination is ordinary implementation. Errors in that implementation can only ever produce detectable counterfeiting because blocks commit to the full contents of every transaction, including its proofs, so history can always be replayed through corrected software.

In our Lean code, the fingerprint is a function called assemble. (The snippet below uses assemble?, its partial form, which reports assembly failures as none; assemble is the total wrapper over it.)

def DeployedAccepts urs hk vk instanceCommitment ps ch : Prop :=
  -- Assemble the verifier's final MSM.
  match assemble? vk instanceCommitment ps ch with
  -- Accept only if the MSM evaluates to the group identity;
  -- `hk` casts it to the URS's size for evaluation.
  | some m => (hk ▸ m).eval urs = 0
  -- Any assembly or well-formedness failure rejects.
  | none => False

By isolating the verifier behind the fingerprint, we avoid reasoning about the Rust code more specifically than our claimed security property requires.

Checking the fingerprint against the implementation is then a matter of running both sides on the same inputs: we run the verifier in halo2 against an instrumented backend that records the challenges the verifier draws and the coefficients of the final combination instead of evaluating it.

Lean proves that assemble reproduces those recorded runs exactly:¹⁹

theorem fingerprint_matches :
    -- Conclusion: Lean's assembled MSM matches the captured Rust MSM.
    MsmMatch (assemble vk derivedInstanceCommitment ps ch) capturedMsm := by
  -- Proof body: compute and check the concrete equality.
  native_decide

The captured runs are validation, not the guarantee itself. Every accepted proof falls into one of two cases, because each one determines a single canonical combination, recomputable from public data. Either that combination evaluates to the group identity, in which case our knowledge soundness analysis applies; or it does not, making the verifier's deviation from the fingerprint public. The real verifier can escape our knowledge soundness guarantee only in ways that are detectable in practice.

Soundness of the Circuit

The fingerprint captures what the deployed SNARK is by describing its verifier algebraically. We showed the formalized verifier is knowledge sound with respect to a particular low-level witness, arriving at the bound we displayed earlier. That witness is a vector of field elements satisfying the equations that the verifier checks, and nothing in that description mentions a note commitment or a nullifier. A high-level witness must be extracted from those field elements for the proof to mean anything to our balance integrity analysis.

We do this with a transcription of the circuit into Lean (built on Clean). The trust boundary remains the fingerprint: the circuit is an algebraic object encoded in the verifying key (one of the fingerprint's inputs), so we reason directly about the equations the low-level witness satisfies, without auditing the circuit's Rust code.

The Action Statement

The high-level witness is judged by a statement of its own, independent of the circuit. In our Lean code that statement is SpecPost, and its content comes straight from the Zcash protocol specification: every clause of the Action statement in §4.18.4, plus the cross-address restriction that NU6.3 introduces.²⁰

An Action is Ironwood's unit of transfer. Each one consumes one note and creates one note, and a bundle carries of them (the same from the knowledge error terms earlier). For each Action, a satisfying witness means:

• correctly derived nullifiers,
• values in range and sound value commitments,
• spends bound to the correct spending key material,
• well-formed note commitments,
• enforcement of the spend and output enable flags,
• membership of the spent note in the note commitment tree (zero-valued dummy spends excepted), and
• an output note addressed to the spent note's own receiver whenever the restriction is active.

The record these clauses constrain holds the Action's public inputs together with the private data behind them (the notes, values, and keys underlying a shielded transaction):

-- Everything the Action statement speaks about: the ten public
-- inputs, then the private witness data.
structure ActionData where
  anchor : Fp
  cvX : Fp
  cvY : Fp
  nfOld : Fp
  rkX : Fp
  rkY : Fp
  cmx : Fp
  enableSpend : Fp
  enableOutput : Fp
  disableCrossAddress : Fp
  psiOld : Fp
  rhoOld : Fp
  nk : Fp
  vOld : Fp
  vNew : Fp
  ...
  cmOld : Point Fp
  gdOld : Point Fp
  akP : Point Fp
  pkdOld : Point Fp
  ...
  merklePath : ℕ → Fp × Fp
  ...

For example, three of the clauses as our Lean code states them:

-- Nullifier integrity:
-- nf_old = Extract([PRF(nk, ρ_old) + ψ_old] K + cm_old).
wit.nfOld = (wit.cmOld
    + (poseidonHash #v[wit.nk, wit.rhoOld] + wit.psiOld) • B.nullifierK).x

-- The anchor check, over the Merkle root recomputed from the witnessed
-- path. Real spends must land on the anchor; dummy spends have v_old = 0.
wit.vOld * (root - wit.anchor) = 0

-- Old note-commitment integrity: wherever the Sinsemilla hash lands,
-- NoteCommit must open to cm_old.
HashGuarded G.S B.noteQ
  (noteScalars wit.gdOld wit.pkdOld wit.vOld wit.rhoOld wit.psiOld).chunks
  (fun bp => wit.cmOld = bp + wit.rcmOld.2 • B.noteCommitR)

The last clause is guarded (HashGuarded): wherever the Sinsemilla hash is defined, the note commitment must open exactly as the protocol specifies. The hash is partial because Sinsemilla's underlying point addition is, and an undefined query is not a free pass; a classifier extracts the incomplete chain from the witness as a concrete break of the underlying hash, in the breaks-as-computed-data convention from earlier.

Balance integrity rests on three of these clauses in particular. Values in range rule out overflow (the trick behind Bitcoin's counterfeiting incident), and sound value commitments tie each Action's hidden values to the transparent value its bundle publicly moves in or out of the pool. Correctly derived nullifiers give every note exactly one nullifier, so the network's rejection of duplicates makes a second spend of the same note collide with the first. And membership means every real spend consumes a note that the pool actually contains.

Each of the three closes a route by which the hidden value stored in the pool could come to exceed the net public value that has flowed into it.

The Circuit Theorems

Extraction from the low-level witness runs through the circuit, whose constraints govern a grid of field elements called cells. An assignment of the cells satisfying every constraint is the circuit-level witness, and an explicit extraction function reads the record above off any such assignment.

The transcription proceeds chip by chip and region by region against the circuit code that ships with NU6.3.²¹

The circuit theorems prove that the constraint system means what it is supposed to mean: any satisfying assignment of the cells yields (through the extraction function) a witness satisfying SpecPost for the same public inputs. Soundness is the contract soundnessPost, as our Lean code states it:

theorem soundnessPost (G : Generators) (B : Bases) (cfg : Config) :
    FormalCircuit.Soundness (Witness := fun _ => ActionData)
      (mainPost G B cfg)    -- the transcribed synthesis
      (extractPost cfg)     -- reads an `ActionData` off the cells
      (EnvAssumptions cfg)  -- table wiring, selector distinctness
      (fun _ => True)
      (SpecPost G B)        -- the Action statement

Completeness is proven alongside (completenessPost), but it is not important for our knowledge soundness analysis since failures in completeness do not enable counterfeiting bugs.

#99 landed the deployed-key reduction that takes an accepting run, on challenges clear of the charged failure surfaces, to the circuit's semantic statement for every Action in the bundle, or to a nontrivial discrete-log relation among the URS generators.

Agreement with the Verifying Key

Given the boundary, the transcription's obligation is agreement with the constraint system encoded by the deployed verifying key, not with the code it was transcribed from. Consulting the code merely makes the proof easier to write.²²

Balance Integrity

Balance integrity is what all of this work is for. It requires that the shielded pool never pay out more value than has publicly flowed into it. Knowledge soundness is one component of the analysis, and covers a single proof at a time. The property concerns an entire ledger, so the last layer of our Lean development reasons about ledgers directly.

The Ledger Model

Our Lean formalization models a ledger as a list of transactions, each carrying its Actions, its declared transparent value balance, and the sighash its signatures cover. ValidLedger transcribes the consensus rules: every Action's witness satisfies the Action statement, no nullifier is revealed twice, every anchor is a root the note commitment tree actually reached at an earlier transaction boundary, and every spend authorization and binding signature verifies.²³ The theorems below quantify over every valid ledger, with no model of the network and no interaction, a superset of anything a real attacker can assemble.

Each Action in the model arrives annotated with its witness. Knowledge soundness is what justifies the annotation. It puts a low-level witness behind every accepting proof, the circuit theorems read an ActionData off it that satisfies SpecPost, and specPost_to_ledger shows that a witness satisfying SpecPost either satisfies the abstract Action statement that the ledger theorems consume or computes a break of the Sinsemilla hash from its own queries.

The Ledger Theorems

Every theorem over this model follows the convention from earlier: the property holds, or the ledger's own contents compute a concrete break.

• Every spend is a committed output (balanceSubsetOrBreak). The nonzero spends across any prefix of a valid ledger form a sub-multiset of the outputs of strictly earlier transactions: each spend opens the exact output that created its commitment, at that output's leaf position, and no output is spent twice. Otherwise the reduction computes a hash collision inside the note commitment tree, a note commitment opened two ways, or a key-binding break.
• Value is conserved (ValueShape.conservationOrBreak). After any prefix of a valid ledger, the pool's hidden value plus the transparent pool's balance equals the total issuance minted so far, so the pool never holds more than came in. Otherwise the reduction computes a nontrivial discrete-log relation between the value commitment bases. The binding signature carries this argument, and we return to it below.
• Received notes stay spendable (spendabilityOrBreak). The owner of a note the pool contains can always extend the ledger with an honest transaction spending it.²⁴ Otherwise the reduction computes the obstruction: an Action that already spent the identical opening, a note-commitment break, or two distinct openings sharing one nullifier, itself a discrete-log relation among the nullifier and commitment bases (NontrivialRelation.ofNullifierCollision). This closes the Faerie Gold attack, in which notes are crafted to share a nullifier so that spending one forfeits the rest.
• Spending requires authorization (spendAuthorityOrBreak). If an Action spends a note addressed to a victim, in a transaction whose sighash the victim never signed, the reduction computes a verifying forgery against a randomization of the victim's spend authorization key, or a key-binding break.²⁵

The Binding Signature

The binding signature ties a bundle's hidden values to the transparent value it declares. Every Action publishes a value commitment to its net value , over fixed bases and , with the randomness hiding the value perfectly. Consensus sums a bundle's commitments and subtracts a randomness-free commitment to the declared amount, yielding the binding verification key , in which is exactly the imbalance between the witnessed values and the declared amount. The transaction must sign its sighash under with base , a Schnorr-style argument of knowledge of with . An imbalanced bundle has therefore presented two representations of one group element over and , and subtracting them is a relation:

-- An imbalanced bundle whose binding signature verifies computes a
-- nontrivial discrete-log relation between the two value bases.
def NontrivialRelation.ofImbalance (V R bvk : M) (A B bsk : F) (hA : A ≠ 0)
    (hExtract : bvk = bsk • R) (hSum : bvk = A • V + B • R) :
    NontrivialRelation V R

A relation between and always exists, just as one did among the URS generators. The assumption forbids computing one. The dichotomy so far gives balance only modulo the group order , not over the integers. The Action statement's range clauses close the gap. Because every value is range-proven and a bundle carries at most Actions, the net value cannot wrap, so a residue of zero forces the integer to be zero (intBalance_eq_zero_of_lt).

Key Binding

The key-binding break that two of the theorems above fall back on has a theorem of its own, ZIP 2005's key-binding theorem: a satisfying witness pins the key material behind its address, or a break is exhibited. We prove that two openings of one key commitment force their committed scalars equal up to sign (commit_scalar_pm), that a break computes a random-oracle collision up to sign, and that producing a collision within oracle queries has probability at most the birthday bound (break_measure_le_adaptive).²⁶

The Probabilistic Capstones

Each property then carries a probabilistic capstone. An adversary is an arbitrary distribution over valid ledgers, a violation lands its reduction in one of the break arms, and the violation's probability is at most the sum of the arms' break probabilities (balanceSubset_measure_le and its siblings). Every break in the ledger layer's vocabulary reduces to the discrete logarithm, to the random oracle, or to the unforgeability of the spend authorization signature; the first two are the same assumptions the SNARK analysis already consumed.

The book's security definitions draw the full dependency picture. The knowledge soundness bound displayed earlier is the largest single piece of that picture, but only one piece: every clause of balance integrity now ends in a machine-checked proof.