Howdy,
We’ve submitted a retroactive grant application to the Coinholder Retroactive Grants Program for Project Tachyon’s work on the Ironwood emergency response:
Requested amount: $738,942. External audit and formal-verification invoices ($225,000), in-house engineering billed at 2× benchmark rates anchored to what we paid those external firms ($506,942), and frontier-model costs ($7,000). The 2× multiplier is an emergency-response premium: this was an unplanned mobilization begun within days, against a fixed activation deadline, displacing all other work. Rush security engagements are billed at 1.5–2× standard rates plus mobilization fees, and emergency mobilization of this class — start within days, no standing retainer — commonly runs 2–3× retained rates; we bill the bottom of that band, and no mobilization fee. The external lines are exact invoiced amounts, the in-house lines are arithmetic on the benchmark rates and the premium, with the work documented in public commit and review history, and the frontier-model line is a conservative estimate, labeled as such in the application. The full application is reproduced below so you don’t have to click away.
About our funding: Tachyon Foundation has previously been funded by private donations from Zcash coinholders, as we have disclosed publicly before, in posts on X (1, 2), in our Zakura announcement, and in zcash/orchard#504. No donation, grant, or contract covered the Ironwood work; the external engagements were floated entirely out of our own funds. Full details are in the application below.
The short version: on May 29, Taylor Hornby discovered a soundness bug in the Orchard circuit that could have allowed undetectable counterfeiting of ZEC. It was patched and publicly disclosed days later, and because Orchard is a shielded pool, patching it could not answer the deeper question of whether the supply was still sound. On June 6 we publicly committed, alongside Valar Group and in coordination with ZF, Shielded Labs, and ZODL, to the Ironwood response; our goal was to lead the formal verification of the Ironwood zk-SNARK. Over the following weeks we implemented the Ironwood circuit changes, engaged and funded two independent verification firms to formalize the soundness of the new circuit, and glued that work to our own machine-checked Lean proofs of the Halo 2 construction, demonstrating that there are no vulnerabilities in the Ironwood zk-SNARK (up to cryptographic assumptions) that would permit undetectable counterfeiting in the new pool. We published the result the day Ironwood activated. The published development totals 2,700+ theorems and includes contributions from external collaborators credited in our announcement.
Jason McGee, Executive Director of Shielded Labs, provided the following statement for this application:
Formal verification was an important part of the security assurance work for Ironwood, and Project Tachyon led the effort to formally verify the Ironwood zk-SNARK in time for activation. Ironwood was one of the most important security upgrades in Zcash’s history because it addressed the uncertainty created by the Orchard vulnerability and re-established confidence that Zcash’s supply limits could be independently verified going forward. Shielded Labs believes Project Tachyon’s work materially strengthened confidence in Ironwood’s soundness and is highly supportive of recognizing it through a retroactive grant.
— Jason McGee, Executive Director, Shielded Labs
Verify in five minutes
- Read the completion announcement (July 28): https://tachyon.z.cash/blog/ironwood-verification-complete/
- Browse the formalization yourself: https://github.com/zcash/ironwood contains 2,700+ Lean theorems. You can machine-check the proof locally by following the build instructions in the repository. If you want a fixed target, commit
591454c22e25cd108a1b3e0726b8daabf006fc51is the repository state at the July 28 completion announcement. - Open https://github.com/zcash/orchard/pull/504, the NU6.3 circuit implementation, opened June 12 and merged June 23 after review.
- Cross-check the timeline: the public commitment on June 6 (https://tachyon.z.cash/blog/auditing-orchard-supply/), the published trust boundary and reasoning on July 7 (https://tachyon.z.cash/blog/detecting-counterfeiting-in-zcash/), and delivery on July 28, the day Ironwood activated.
What this application does NOT claim
To keep the scope clean: we claim nothing for ZODL’s independent ledger-security and balance-integrity work (that is theirs); nothing for the post-activation adversarial strengthening and third-party audits of the formalization we are currently funding (possibly a future application); nothing for Project Tachyon’s own protocol work; and nothing for the delay to our roadmap or the burden on the rest of our team: real costs we chose not to price.
Additional Team Members
- name: Tal Derei
role: Formalization Lead (Tachyon's Lead Engineer)
background: Formerly a cryptographic engineer at Penumbra; developed ZK circuits
and GPU-accelerated proving systems across both server and client-side proving,
with experience formalizing circuits in Lean through Tachyon's existing formal
verification work
responsibilities: Full-time lead of the Lean formalization of the Ironwood zk-SNARK
verifier, covering the algebraic verifier model, knowledge-soundness security
notions, and integration with circuit soundness
Project Summary
After an undetectable counterfeiting vulnerability in Zcash’s Orchard pool was publicly disclosed in early June, Project Tachyon paused its roadmap to lead the formal verification of Ironwood (the successor pool shipped in NU6.3), with a focus on eliminating the entire class of undetectable counterfeiting bugs. We implemented the new Ironwood circuit changes, engaged and funded two independent verification firms to formalize the soundness of the new circuit, and glued that work to our own machine-checked Lean proofs of the Halo 2 construction, demonstrating that there are no vulnerabilities in the Ironwood zk-SNARK (up to cryptographic assumptions) that would permit undetectable counterfeiting in the new pool.
Project Description
Background. On May 29, 2026, Taylor Hornby discovered a soundness bug in the Orchard zk-SNARK circuit that could have allowed an attacker to undetectably counterfeit ZEC. The bug had existed since Orchard activated four years prior. It was quickly remediated by the Zcash Open Development Lab (ZODL), and it is widely believed that the vulnerability was never exploited.
Nevertheless, following public disclosure there was a large crisis of confidence given the size of the shielded pool and the possible risk of exploitation, leaving the circulating supply of ZEC in doubt among users and investors. The community and various Zcash development organizations quickly rallied around Shielded Labs’ proposal to create a new pool based on Orchard that patched the vulnerability from inception and underwent additional scrutiny to minimize the risk of further bugs.
The newly discovered bug had been present in the codebase for years despite extensive auditing and an enormous (implicit) bounty for malicious exploitation. Our team immediately announced a plan to formally verify the Ironwood zk-SNARK to eliminate the class of undetectable counterfeiting bugs from the new protocol entirely. Our readiness was no accident: we have been developing a new shielded pool for Zcash, and we already had contracts in place for developing and integrating formal proofs as part of our own assurance efforts. In fact, we had just published an article describing these efforts, which was very useful in communicating the practicality of the approach during the chaotic days following disclosure.
Our commitment. On June 6, 2026, together with Valar Group and in coordination with the Zcash Foundation, Shielded Labs, and ZODL, we publicly committed to the Ironwood response. Our team’s goal was to lead the formal verification of the Ironwood zk-SNARK, diverting our own resources to the project, and collaboratively engaging with other teams and firms at our own expense.
This was an extremely ambitious goal. NU6.3 was slated to activate within two months, and formal verification of a deployed cryptographic protocol is normally an effort measured in years. The required expertise is also scarce; we are Zcash protocol experts and our team includes a principal author of halo2, so we were among the few teams positioned to attempt this on such a short timeline.
Our results. We redirected our entire formal verification program (including standing engagements) to Ironwood:
- Circuit implementation. We developed the post-upgrade Orchard/Ironwood Action circuit and supporting
orchardcrate changes. Finalizing the circuit early gave every analysis team a stable target and enabled Ironwood testnet development within two weeks of the announcement. - Independent external verification, funded at our expense. Halo 2 circuits use a fully custom, highly structured arithmetization that fits no existing verification framework, and the timeline was too tight to bet on a single team. We therefore engaged both zkSecurity and Formal Land to formally analyze the circuit, ensuring at least one path to success and mutual assurance if both succeeded.
- The zk-SNARK formalization. Our team designed and executed the core strategy: treat the specified verifier as an algebraic function over the group and prove knowledge soundness of the zk-SNARK against that object. This trust boundary is the minimum necessary to rule out undetectable counterfeiting arising from a mistake in the zk-SNARK construction (circuit or protocol). We published the reasoning in Detecting Counterfeiting after Zcash’s Ironwood and the scope of the verifier model in the completion report’s verifier fingerprint section.
- Delivery. On July 28, 2026, we announced the machine-checked result: a Lean formalization of the Ironwood SNARK verifier, the security notions capturing knowledge soundness, and the glue to circuit-soundness results, public at github.com/zcash/ironwood. The published development totals 2,700+ theorems and includes contributions from collaborators credited in our announcement, including Gregor Mitscha-Baude of zkSecurity and Daira-Emma Hopwood of ZODL; the parallel independent soundness proof by Formal Land’s Guillaume Claret and Valerii Huhnin is acknowledged there as well.
Scope.
- Claimed by this application: (a) the NU6.3/Ironwood circuit and consensus rule implementation, meaning the post-upgrade Orchard/Ironwood Action circuit and supporting
orchardcrate changes; (b) the primary Lean formalization of the Ironwood zk-SNARK, meaning the algebraic verifier model, the knowledge-soundness security notions, and their integration with circuit-soundness results (published); (c) the design and coordination of the verification effort, including the two parallel external engagements we funded; (d) the public assurance communications that defined and reported the effort, especially our published trust boundary and our completion report. - What the verification establishes (and does not): it rules out undetectable counterfeiting bugs originating in the zk-SNARK construction (circuit or protocol specification), up to explicitly named cryptographic assumptions, within the published trust boundary. It deliberately does not cover implementation bugs (these produce detectable counterfeiting, discoverable through retroactive auditing of the chain) or failures of cryptographic assumptions (vulnerabilities of that kind are not bugs in the construction, and no formal verification can exclude them). These exclusions were published up front.
- Not claimed by this application: any balance integrity proofs, ledger games, formalizations of assumptions or other contributions produced independently by ZODL. That work is theirs, this application does not depend on it, and we will not overlap with any application they may submit. Also not claimed: post-activation adversarial strengthening of the formalization and subsequent third-party audits of it, which are ongoing at our expense and may be the subject of a future application.
- Indirect costs: the emergency response consumed more than the itemized work below. For two months, our roadmap stalled: the rest of our team continued executing Project Tachyon with sharply reduced guidance and support while the two of us were consumed by Ironwood, and the external engagements were paid out of the audit budget reserved for our own project’s assurance work. We claim none of that indirect cost in this application. No roadmap-delay line, no opportunity cost, no compensation for team members whose work was burdened rather than redirected. This application prices only the completed Ironwood work itself.
Technical Approach
- Black-box algebraic verifier model. We modeled the specified behavior of the Ironwood SNARK verifier as an algebraic function over the group and formalized knowledge soundness against this object. This captures both circuit bugs and bugs in the SNARK protocol itself while presenting a single, clean, publicly communicable trust boundary: the minimum necessary boundary for the undetectable-counterfeiting class.
- Lean 4 formalization of the verifier, the knowledge-soundness security notions, and the connection to circuit-soundness results, developed in less than two months under activation deadline pressure and published in full.
- Parallel external engagements with zkSecurity and Formal Land for circuit-level analysis, deliberately redundant to de-risk the timeline; zkSecurity’s circuit-analysis framework (Clean) used for circuit soundness.
- Circuit and consensus rule implementation in the
orchardcrate via zcash/orchard#504, including the shared post-upgrade Action circuit and bundle-semantics API changes, merged after external review. - AI-assisted development and auditing, disclosed publicly at the time (in our commits and in zcash/orchard#504): frontier-model assistance for Lean development and implementation work, plus preliminary auditing passes with zkao (within the zkSecurity engagement) and v12 (we did not pay for our usage; nothing claimed). Lean formalization at this pace and scale is frontier-model-intensive; our model usage is included in the budget.
Time Period of Work Completion
June 1, 2026 – July 28, 2026
Total Budget (USD)
$738,942
Budget Breakdown
Basis of valuation: External engagements are billed at their exact invoiced cost: $225,000 paid by Tachyon Foundation with no reimbursement from any source; we are happy to provide the underlying invoices privately to FPF for verification upon request. In-house work is priced at market rates for specialized zero-knowledge formal-verification and cryptographic engineering, anchored to the arm’s-length rates we ourselves paid within this same effort: our benchmark staff engineering rate equals the per-engineer-week rate of our external formal-verification engagement, and the benchmark principal rate reflects standard market structure for lead/principal engineers (the invoices offered to FPF substantiate both). Because this was an emergency engagement — an unplanned mobilization begun within days of disclosure, against a fixed activation deadline, displacing all other work — in-house time is billed at 2× those benchmark rates. Firms taking rapid, unplanned security engagements charge premiums of 1.5–2× standard rates plus mobilization fees, and engagements in this specific class — an emergency start within days, with no standing retainer — are commonly billed at 2–3× retained rates in the incident-response market; an external firm taking this engagement (if one with the requisite halo2 expertise had existed at all) would have priced it in those bands. We bill 2×, at the bottom of the emergency-mobilization band, apply it to the rate only, and charge no mobilization fee. Sustained overtime during the emergency is billed as time (standard week-equivalents at the premium rate), not as a further rate increase. The circuit-implementation window and the July formalization intensity are directly visible in public commit history (zcash/orchard#504, GitHub - zcash/ironwood: Formal Verification of the Zcash Protocol and Documentation for the Ironwood Pool · GitHub); the June design and review work is documented in the PR #504 review record, and we can substantiate the full allocations privately to FPF.
- Compensation:
- $(USD): $506,942
- Justification: Compensation for the two of us who worked on Ironwood in-house from June 1 to July 28, 2026. That period is 58 days; we bill it exactly, as 8 2/7 weeks, with fractional dollars rounded down. All in-house time is billed at 2× our benchmark rates, the emergency-response premium described in the basis of valuation above.
Tal Derei led the Lean formalization: the algebraic verifier model, the knowledge-soundness security notions, and their integration with circuit soundness. This began in June with the verifier model's design and review of the circuit implementation (zcash/orchard#504), and later included the verifier fingerprint fixtures connecting the formalization to the implementation (zcash/orchard#531, #538). He worked the full period at a sustained ~60-hour pace under the activation deadline, billed as 12 3/7 standard engineer-weeks (8 2/7 weeks × 60 hours, against a 40-hour standard week) × $25,000/week (2× the $12,500/week benchmark) = $310,714. The benchmark rate equals the per-engineer-week rate we paid at arm's length for our external formal-verification engagement within this same effort, and the overtime is billed as additional week-equivalents, not as a further rate increase.
Sean Bowe implemented the NU6.3 circuit changes: the post-upgrade Orchard/Ironwood Action circuit and the supporting orchard-crate changes (zcash/orchard#504), full-time for 2 weeks × $34,000/week (2× the $17,000/week benchmark) = $68,000.
Sean Bowe then led the verification effort for the remaining 6 2/7 billed weeks: trust-boundary and scope design, mathematical review and strategy for the formalization, coordination of the external firms, public assurance communications, and the engineering that carried the circuit into activation, including its integration into orchard's main branch (zcash/orchard#516), a testnet-safety consensus check (zcash/orchard#513), and the crate releases used by the activation (zcash/orchard#533, #540). This is billed at a 60% allocation, 6 2/7 weeks × 60% × $34,000/week = $128,228. The benchmark principal rate ($17,000/week) reflects standard market structure for lead/principal engineers relative to the staff benchmark (1.36×).
- Technology/Software:
- $(USD): $7,000
- Justification: Frontier-model usage for the Lean formalization and implementation work. Lean development at this pace is frontier-model-intensive, and our use of AI assistance was disclosed publicly in zcash/orchard#504 at the time of the work. The estimate is conservative: our model usage is not accounted on a per-repository or per-task basis and is spread across providers, OpenAI and Anthropic. We can provide provider billing statements for the period privately to FPF on request; they show combined usage across all of our work, which is why we claim a conservative estimate rather than an exact figure. The v12 auditing tool was also used; we did not pay for that usage and nothing is claimed for it (see Conflict of Interest Disclosure).
- Infrastructure/Hosting:
- $(USD): $0
- Justification: Not claimed.
- Services/Contractors:
- $(USD): $225,000
- Justification: We engaged two independent external firms in parallel to de-risk the activation timeline, paid entirely by Tachyon Foundation. [zkSecurity](https://zksecurity.xyz/)'s $150,000 engagement covered three workstreams: a circuit security audit, continual AI-assisted auditing via zkao, and formal verification work. The audit ran alongside our circuit development deliberately: we wanted circuit bugs found and fixed early, before the formalization had gone deep enough that circuit changes would force it to be redone, and before any bug could ship in the activation. [Formal Land](https://formal.land/)'s $75,000 engagement was an independent backup formalization of the zk-SNARK circuit in case the primary circuit-analysis path failed.
- Other:
- $(USD): $0
- Justification: Not claimed. We explicitly exclude the post-activation adversarial strengthening and third-party audits of the formalization, which are ongoing at our expense and may be the subject of a future application; ZODL's independent ledger-game and balance-integrity work; and all Project Tachyon protocol development, including the ~2-month roadmap delay and the burden on team members who continued our core project with reduced guidance and support during the pivot. These are real costs, but we have not priced them here.
- Total $(USD): $738,942 ($506,942 compensation + $7,000 technology + $225,000 services/contractors)
Previous Funding
Tachyon Foundation has not previously received funding from the Zcash Coinholder Grants Program.
Other Funding Sources
Tachyon Foundation has previously been funded by private donations from Zcash coinholders, as we have disclosed publicly in posts on X (1, 2), in our Zakura announcement, and in zcash/orchard#504. Our donors are anonymous, but we operate with full independence from them, and we have no ongoing pledged financial support. We have formed a 501(c)(4) under the auspices of Wyoming and are currently undergoing the IRS approval process as required under the Internal Revenue Code. No grant, contract, or donation was received for the Ironwood work: it was an unbudgeted emergency reallocation that consumed funds earmarked for the audit and assurance budget of our own project, and the $225,000 of third-party engagements itemized above were floated entirely out of our own funds. No other funding source covers, or is expected to cover, any item in this application.
Success Metrics
-
The existential question was answered. The published, machine-checked proof (2,700+ theorems), completed in parallel with Ironwood’s activation, established that there are no vulnerabilities in the Ironwood zk-SNARK (up to cryptographic assumptions) that would permit undetectable counterfeiting in the new pool.
-
Schedule. The June 6 statement targeted activation on an emergency timeline of under two months. Our circuit changes, opened June 12 and merged June 23, enabled Ironwood testnet development within two weeks of the announcement; Ironwood activated on mainnet July 28, 2026, with the machine-checked verification published the same day.
-
Ecosystem confidence restored, concretely including coinholder governance itself: the Q2 2026 coinholder vote was postponed due to the Orchard vulnerability; the Q3 poll (in which coinholders will consider this application) is possible because confidence in the supply was re-established, through the remediation and the verification work.
-
A new assurance standard for Zcash. No previous Zcash shielded pool shipped with formal verification of its SNARK. The formalization, security notions, and methodology are public and reusable for future upgrades.
-
Acceptance. The code and specification changes we produced were reviewed, merged into the protocol itself, and shipped in the Ironwood activation. As the June 6 joint statement records, the formal verification effort was an explicit, publicly stated goal of the Ironwood upgrade, and we delivered it. And Shielded Labs’ own Ironwood page thanks “Project Tachyon, Valar Group, and ZODL for helping define Ironwood’s architecture, implementing the new consensus rules, and carrying out the critically important formal verification work.” Jason McGee, Executive Director of Shielded Labs, provided the following statement for this application:
Formal verification was an important part of the security assurance work for Ironwood, and Project Tachyon led the effort to formally verify the Ironwood zk-SNARK in time for activation. Ironwood was one of the most important security upgrades in Zcash’s history because it addressed the uncertainty created by the Orchard vulnerability and re-established confidence that Zcash’s supply limits could be independently verified going forward. Shielded Labs believes Project Tachyon’s work materially strengthened confidence in Ironwood’s soundness and is highly supportive of recognizing it through a retroactive grant.
— Jason McGee, Executive Director, Shielded Labs
Proof of completion
- Repository/Commit:
- [github.com/zcash/ironwood](https://github.com/zcash/ironwood): the complete Lean formalization (verifier model, knowledge-soundness notions, circuit-soundness glue). 2,700+ theorems, machine-checked, public. Commit 591454c22e25cd108a1b3e0726b8daabf006fc51 is the repository state at the July 28 completion announcement; build instructions are in the repository.
- [zcash/orchard#504](https://github.com/zcash/orchard/pull/504): NU6.3 circuit implementation. Opened June 12, merged June 23, 2026.
- Publication:
- [Ironwood: Auditing the Orchard Pool's Supply](https://tachyon.z.cash/blog/auditing-orchard-supply/), June 6, 2026: joint public commitment (with Valar Group; ZF, SL, ZODL aligned)
- [Detecting Counterfeiting after Zcash's Ironwood](https://tachyon.z.cash/blog/detecting-counterfeiting-in-zcash/), July 7, 2026: published trust boundary, reasoning, and goals, in advance of completion
- [Formal Verification of Zcash Ironwood Completed](https://tachyon.z.cash/blog/ironwood-verification-complete/), July 28, 2026: completion announcement with contributor attribution
- Deployment/Release:
- Ironwood (NU6.3) activated on Zcash mainnet on July 28, 2026, using the finalized circuit from zcash/orchard#504, with the verification published the same day
- Other Evidence:
- [Shielded Labs' account of the vulnerability](https://shieldedlabs.net/the-orchard-counterfeiting-vulnerability/): independent timeline of the crisis this work responded to
Conflict of Interest Disclosure
These are ordered by what we consider the most significant conflicts first.
- Tachyon Foundation has previously been funded by private donations from ZEC holders, and because those donors may still be coinholders today, they may also participate in the coinholder vote on this application. We have no knowledge of, or influence over, their voting decisions, and they exercised no direction over the work described here. Our funding source is a fact we have disclosed publicly on multiple occasions (see Other Funding Sources Details), and those donors stand to benefit from ecosystem-wide supply assurance in the same way all coinholders do.
- Sean Bowe is an investor in v12 (a Zellic product), an AI-assisted auditing tool; he has disclosed this investment publicly (post on X). We used v12 for preliminary auditing passes during this work, a use we disclosed in zcash/orchard#504 at the time, and we have used it elsewhere in our work as well. We did not pay for our v12 usage, and no v12 costs are claimed in this application. Beyond that self-serve tool usage, Zellic was not engaged by Tachyon Foundation and performed no services on any work in scope for this application. For the avoidance of doubt, we hold no investment or financial interest in zkSecurity or Formal Land, the firms we engaged.
- Contributors to the verification effort included individuals affiliated with other organizations (e.g., Daira-Emma Hopwood of ZODL, Gregor Mitscha-Baude of zkSecurity); their contributions are acknowledged in our publications. ZODL’s independent formal work (ledger security games, balance integrity) is not claimed by this application, and we will not overlap with any application ZODL may submit for it.
- zkSecurity holds other engagements with Tachyon Foundation (Ragu audit/verification) that are unrelated to and not claimed by this application.
- Sean Bowe was previously a long-time engineer/cryptographer at the Electric Coin Company and is an author of much of the cryptography underlying Zcash (including Sapling and Halo 2); Project Tachyon works closely with the organizations named in this application.
- Tachyon develops Zcash node software (Zakura) together with Valar Group, our co-author on the June 6 joint statement; that work is outside the scope of this application.
- Tachyon Foundation has no financial, contractual, or governance relationships with the keyholder organizations (the Zcash Foundation, Shielded Labs, and the Financial Privacy Foundation) beyond the public inter-organizational coordination described in this application.
- We have formed a 501(c)(4) under the auspices of Wyoming and are currently undergoing the IRS approval process as required under the Internal Revenue Code.
