Over the last several months our team has been developing Tachyon, a new shielded protocol for Zcash that addresses several of the fundamental scaling challenges inherent to our no-compromise privacy tech. In parallel, we have been developing a new Rust-language recursive zk-SNARK toolkit called Ragu which serves as the fundamental platform upon which Tachyon's cryptography is constructed.
Ragu is purpose-built to support Tachyon's needs and practical constraints. It aims to be a production-grade realization of the original Halo paper that introduced efficient ECDLP-based recursive SNARKs to the literature without the use of trusted setups. In many ways, it is a manifestation of what some would call "recursive Bulletproofs."
Simpler Foundations
In the spirit of risk aversion, Ragu leans heavily on tools we have already shipped in Zcash: the Pasta elliptic curve cycle, the original Poseidon algebraic hash function, univariate polynomial multi-commitment schemes using inner product arguments—all of which we deployed in Orchard years ago. In fact, Ragu largely avoids cryptography older than 2021, using familiar assumptions and security models.
In sharp contrast to the hand-optimized PLONK-based arithmetization used to implement Orchard's zk-SNARKs—developed in the halo2 library—Ragu relies on a simple R1CS-like recipe based around the [BCCGP16] lineage of protocols.
Most recent constructions use sum-check protocols over multilinear extensions to achieve state-of-the-art performance, but Ragu can achieve asymptotically equivalent results in our setting through the straightforward application of (split) accumulation schemes and related techniques. Ragu's arithmetization gives rise to a very simple univariate polynomial IOP based on the (embarrassingly linear) verifier check
where 
denotes the dot product of two vectors with one reversed, and 
are random verifier challenges. This can be written in terms of univariate polynomial oracles and compiled into a SNARK using standard techniques. And thanks to additively homomorphic Pedersen commitments, we can accumulate and fold our way into a recursive SNARK.
In addition to the simpler core protocol, Ragu's design accommodates several other features that are crucial for Tachyon:
- Ragu works within the non-uniform PCD model, where each node in the computational graph can choose to draw upon many possible functionalities and pay only for the ones actually used in that step. This model becomes absolutely necessary for most PCD applications anyway, and Ragu embraces it heavily: instead of optimizing individual circuits using custom, complicated arithmetizations, we partition our subprotocols into many different circuits that execute simultaneously.
- The entire construction revolves around univariate polynomial commitments, which are sufficient to encode Ragu's circuits and enable the accumulation and folding operations. The underlying proving system exposes the ability to query polynomial oracles within application-level circuits themselves, which Tachyon depends on for various subprotocols.
- Verification performance does not rely on any pre-processing, which would force our arithmetization into another shape with a different cost model. Instead, the polynomials that represent dense circuit encodings are designed to be succinct, using a circuit development API that induces structures within those polynomials that the verifier can leverage to efficiently evaluate them. We use a technique from the original Halo paper to accumulate claims about evaluations of public polynomials that describe our circuits, and this arrangement facilitates a novel "collaborative" setting that we'll discuss in a future post.
High Assurance Engineering
Ragu’s cryptographic design and implementation have been developed in conjunction with each other. As we've iterated, we've also sought feedback from experts to inform design decisions and focus our efforts on defensive security engineering. In addition to audits, extensive testing and the application of AI analysis tools, we use a combination of fuzzing and targeted Lean-based formal verification tools to provide additional assurance.
Formal Verification
There has been a surge of interest in formal verification techniques and machine-assisted proofs in the cryptography space, with Signal's recent post-quantum ratcheting implementation being a notable example. In addition to LLM-assisted auditing, we think that formal verification will be a central component of all future cryptographic development work.
Ragu uses a special circuit synthesis API that is designed to accommodate the just-in-time evaluation, circuit "post-processing" and non-uniform PCD architecture that our underlying protocol operates within. But despite the custom-tailored nature of our API, its surface is very minimal and familiar to those who have previously used bellman or arkworks.
We've capitalized on this simplicity, and that of our core R1CS-like circuit model, to begin formally verifying the circuits and gadgets within our construction using zkSecurity's clean formal verification framework for circuits. We consulted with zkSecurity themselves to adapt our API to be compatible with those tools and to integrate their automatic checks into our CI pipeline.
The integration effort here spans two domains:
- Rust-side. a decorated version of our core APIs logs Ragu's constraints and witnesses as Lean syntax: the "Autogen".
- Lean-side. Clean's circuit DSL definitions are adapted to match Ragu's gadgets. Preconditions (assumptions), specifications (postconditions) and soundness/completeness theorems are associated with each primitive component. This ties together with the exported "Autogen", proving they produce identical operation sequences.
The trust boundary is clearly defined across two axes: provider (who wrote it) and trust (how the component is reviewed; by humans? third-party audit? machine check?) Components split on the provider axis into circuit developer contributions, such as the gadget spec, Clean's own tooling, and the Lean kernel itself. This careful delineation ensures that untrusted components can be black boxed, and even (independently) LLM-generated.
Fuzzing
Many projects like ours use automated fuzzing techniques, and the ones we have begun incorporating also revolve around zkSecurity's work on fuzzing ZK circuits. We also borrow heavily from Aztec's techniques for fuzzing their own circuits: techniques from differential fuzzing, instruction vector fuzzing and other kinds of defensive testing.
Documentation
Quality documentation and specifications are both unavoidable requirements, even in a regime dominated by machine-assisted proofs and LLMs. Brian Cantwell Smith observed back in 1985 in The Limits of Correctness: formal verification proves "relative consistency." The program matches the spec, not necessarily that the spec faithfully captures what we're trying to build.
We have been writing a dense book documenting our cryptography as we've been developing Ragu. We have spent countless tokens subjecting this documentation to stochastic review, and while this book is largely unfinished we have already identified major improvements to our codebase and our protocol solely due to review enabled by writing this user-facing documentation.
Tachyon itself will be fully specified (as required by the ZIP process), but we will also attempt to more rigorously specify Ragu especially in comparison with the halo2 library, which was less-carefully specified with respect to the overall Zcash protocol spec.
Guiding Philosophies
Tachyon has many moving parts, and Ragu is probably the most complicated of them. We have been eager to concentrate complexity where it is unavoidable, while keeping all other components as simple as possible: there is no reason to use something more complicated for additional performance if our construction already fits within our targets.
Zcash's conservative vigilance and high assurance approach to cryptographic engineering must be reflected in our work, especially as Zcash rapidly enters the era of private money at scale.