Grant Application - Formal Verification of Consensus Arithmetic and Parsing in zebra-chain

[Natalie]

Hello everyone,

Runtime Verification is submitting a proposal to formally verify consensus-critical arithmetic and parsing in zebra-chain using our Rust → Aeneas → Lean 4 pipeline.

What We Will Verify

Three groups of functions that every Zcash transaction and every block validation passes through:

• Amount (monetary arithmetic): checked_add, checked_sub, Mul<u64>, Neg, Constraint::validate. Every value-balance check in every transaction depends on these. A bug can mint or burn ZEC.

• CompactSize64 (serialization): round-trip on all four encoding bands, length bounds, panic-freedom. Every length prefix in every wire-format message goes through this code. A bug can cause two nodes to interpret the same bytes differently, splitting the chain.

• Height (block-height arithmetic): Add<HeightDiff>, Sub<HeightDiff>, range checks, round-trip identity, monotonicity. Every activation comparison (Sapling through NU6 and beyond) reads from this. A bug can cause nodes to apply different rules at the same height.

These three groups form the deterministic arithmetic and parsing foundation that the rest of the consensus path is built on. We start here because everything above depends on them being correct.

Why This Matters

Testing and code review catch many bugs but cannot cover all inputs. Formal verification produces a machine-checked proof covering every input. The Lean 4 kernel independently re-checks every proof, so the guarantee does not depend on trusting any tool or reviewer, only the kernel. The same class of bug we guard against here (non-minimal CompactSize encodings causing interpretation mismatches) is what caused Bitcoin’s CVE-2012-2459.

Roadmap

This pilot is Phase 1 of an eight-phase programme covering the full consensus arithmetic and parsing layer of zebra-chain (approximately four to six months total). The phases include CompactSize canonicity, LockTime serialization, Proof-of-Work target encoding (256-bit), block subsidy and halving, BIP-34 coinbase height parsing, NetworkUpgrade activation logic, and Merkle tree on transactions. Once this layer is fully verified, the natural next target is the cryptographic primitives layer: Pedersen hashes, note commitments, and the Sapling and Orchard circuits.

Our Pipeline and Track Record

We operate a verification pipeline documented in our blog post and arXiv paper. Under the Ethereum Foundation’s zkEVM Verification Project, we applied it to Plonky3 FRI folding and field arithmetic (Verified-zkEVM/rust-lean). We also verified the size-class arithmetic core of Zooko’s smalloc allocator (runtimeverification/smalloc-verify). We are upstream contributors to Aeneas (#832, #833).

Deliverables

At least eighteen Lean 4 theorems, all kernel-checked with no sorry, covering functional correctness, round-trip properties, and panic-freedom. A public repository with CI rebuilding all proofs on every commit. A final report documenting the pipeline, theorem list, limitations, and the full roadmap.

Budget and Timeline

$30,000 over 4 weeks:

• $15,000 at milestone 1 (end of week 2): Groups A and C proved, at least 12 theorems

• $15,000 at milestone 2 (end of week 4): all three groups proved, at least 18 theorems, final report, public CI repo

As this is our first engagement with the Zcash ecosystem, we are flexible on pricing and see this pilot as an opportunity to demonstrate the value of formal verification for Zcash.

Full proposal details: ZcashCommunityGrants/zcashcommunitygrants#324

We welcome feedback and questions.

[hanh]

Hi @Natalie — is there prior work that takes the approach described in the proposal? I’d like to understand what the full pipeline looks like, using the EVM as an example: starting from a running implementation of a key concept, all the way through to a formal verification of the correctness of its design and implementation.

Thanks,

--h

[readymouse]

I would like to add that I met 2 other team members (Danny and Mark) from the Runtime Verification team during Berlin Blockchain week. While I did not get a chance to talk to Natalie or the specific team proposing this work, and I can 100% say they are real humans and not an AI-generated proposal.

[Natalie]

Hi, thank you for the question!

The clearest prior example is our ongoing work under the Ethereum Foundation’s zkEVM Verification Project. The public artifacts are here:

GitHub - Verified-zkEVM/rust-lean: Verification of Rust code in Lean 4

Let’s take FRI folding from Plonky3 for example, a real function in a real proving system (you will find it’s verification with our pipeline in the repo). So this is the pipeline:

1. Start: the actual Rust source, fold_step / fold_arity, as it runs in Plonky3.
2. Translate: we lift that Rust into Lean 4 with Aeneas. The output mirrors the Rust semantics, so we’re reasoning about the real code, not a hand-rewrite. (See the aeneas-FRI directory.)
3. Specify: we write, by hand, a Lean predicate (Lemma, Theorem) that says what the function should do, the mathematical property it must satisfy.
4. Prove: we prove the translated code satisfies that spec, checked by the Lean kernel.
5. Reproduce: it builds with lake build, so we can use CI to re-run the proofs on every commit, so anyone can clone it and confirm.

The repo has several of these, each self-contained with its own README and status: FRI folding (both Hax and Aeneas pipelines), Horner evaluation with its CompPoly spec, field arithmetic for Plonky3’s Mersenne31, and Merkle inclusion from RISC Zero.

There is also this blog post we wrote (describes pipeline):

From Rust Code to Mathematical Proof: How We Verify Safety-Critical Rust

There is also preprint in Arxiv (our “Experience report paper”):

A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report

For the Zcash pilot the steps are identical. The difference is the target.

But Daira-Emma on the latest Arborist Call said that it would be very useful to verify formally crypto-related parsing… so I am working on another proposal (which would be really useful for Zebra).

And in current proposal we suggest to verify arithmetic core… the base everything else stands on (each transaction depends on these functions we are suggesting to verify).

@hanh please let me know did I answer your question? And you are asking about EVM - that project verifies the cryptographic and arithmetic primitives, not the EVM opcode semantics themselves.

Thanks!

[Natalie]

Yes, thank you! Danny and Mark are both on our team. I asked Mark to track down someone from Zebra and ask which code they’d most want verified… I also told him to pinch a few people, just so everyone’s sure he isn’t a hologram.

[hanh]

Thanks @Natalie , that is indeed what I was looking for.

My concern is that, based on the proposal and the repositories I reviewed, the methodology appears to have been applied only to small, isolated components. The previous work seems to focus on similarly limited examples, while the proposed work covers utility classes such as Amount and CompactInt.

If I have overlooked other verification efforts that target more substantial components, I would appreciate being pointed to them.

Otherwise, my concern is that the proposal demonstrates the methodology only on relatively small pieces of the implementation. It is therefore difficult to evaluate whether the approach would scale to more complex and security-critical areas, such as cryptographic primitives, protocol state transitions, consensus rules, or the interactions between these components.

More generally, I am also trying to understand the practical benefits this methodology is expected to provide. Since the verified components are relatively small and isolated, it is not yet clear to me how much confidence this adds to the correctness or security of the implementation as a whole. Could you elaborate on the concrete benefits you expect from this work? For example, are there classes of bugs that you believe this approach is particularly effective at preventing, or is the longer-term goal to extend the methodology to larger portions of the implementation?

[Natalie]

Yes, you understood correctly. Let me answer the two parts honestly.

On scale and composition. You’re right that most of the public artifacts are component-level. The one place we’ve started reaching past a single function is the FRI work, where we connect the Aeneas-extracted Rust to an independent mathematical spec from ArkLib.

It’s in rust-lean/aeneas-FRI/fold_arity_lean at main · Verified-zkEVM/rust-lean · GitHub , file FoldingCorrectness.lean.

I want to be precise about its status: one theorem through that bridge is fully proved (compute_log_arity_gives_folding_degree), four more are stated but not yet discharged, and right now the Aeneas-side properties are axiomatized on the ArkLib side because of an import conflict (BitVec.toNat_pow is defined by both Aeneas and MathLIb’s Batteries, so they can’t yet live in one file). We’re fixing that upstream (we are active contributors to Aeneas, ArkLib and CompPoly).This specific one was fixed, by the way in my PR in Aeneas. So it’s an honest work-in-progress, not a finished whole-system proof. But it’s the piece that matters for your question, because it’s where the extracted code meets a separately-written specification, which is exactly the design-vs-implementation link.

What the rest of the prior work demonstrates is that the pipeline handles real production code with real complications: generic Rust, field arithmetic with wraparound, iterator-based folds, bit-level reasoning. Those are the things that usually break extraction. So the honest summary is: the method is proven to work on real code, and we have an early, partial bridge to a higher-level spec, not yet a verified subsystem end to end.

On the word “small.” I’d separate two meanings. These functions are small in lines of code, but not small in reach. Amount and CompactSize64 are on the path of every transaction and every block. A utility by size, load-bearing by traffic. We start here because the blast radius is large and the proof cost is low, which is the right ratio to open a programme on.

On concrete benefits. The approach is strongest against a specific set of bug classes, and I’d rather name them than claim general “correctness”:

• Integer overflow / underflow in monetary arithmetic, the kind that mints or burns value. Proven absent over all inputs, not sampled ones.
• Non-canonical / malleable encodings, where two byte strings decode to the same value or one node accepts what another rejects. A consensus-split and malleability class. CompactSize canonicity is exactly this.
• Panic-on-malformed-input, an availability / DoS class: the decoder must return an error, never panic, on hostile bytes.
• Off-by-one and boundary errors in range checks, e.g. height bounds at activation edges.

For these, exhaustive testing can’t cover the input space and review misses edge cases. A proof closes them with certainty. That’s the confidence it adds: not “the system is correct,” but “this class of failure is absent on these functions. Mathematically proved (by induction or other method…).”

On the longer term. Yes, the explicit goal is to extend up the stack. The roadmap moves from utilities to logic with real component interaction: PoW target encoding, NetworkUpgrade activation, transaction Merkle trees. Crypto primitives are the layer above that, a separate and larger effort. Starting at the base lets you evaluate the method cheaply before committing to the harder targets. The pilot is partly a real deliverable and partly a way for you to judge whether the approach earns the larger scope.

If useful, I can sketch what a composed property would look like for Zcash specifically, e.g. tying Amount arithmetic and CompactSize parsing together at the transaction-balance level, so you can see where this goes beyond isolated functions.

[hanh]

The methodology is interesting, but I think this proposal gets the value equation backwards.

The pilot targets three utility types — Amount, CompactSize64, Height — proving no overflow, round-trip, and panic-freedom. A bug in these functions would be high-consequence: they sit on every transaction path. But they’re thin wrappers over checked integer operations; the probability of a bug surviving review is near zero. High consequence × near-zero probability is still near-zero expected value. The proposal is reducing a risk that barely exists.

That said, there is a case for a trial run of the pipeline on Zebra code. If we wanted to close that epsilon of residual risk and get a concrete demonstration of the end-to-end process — from zebra-chain Rust through Aeneas extraction to kernel-checked Lean — these three functions are reasonable targets. But, the proofs would largely be by omega, but that’s fine: they’d show the extraction works on real Zcash dependencies, which is a genuine deliverable.

The problem is the price and the framing attached to it. At $30,000, this is being sold as formal verification of consensus code, when the deliverable is really pipeline integration on three utility functions whose proofs are straightforward. And the roadmap doesn’t fix it: phases 1–7 are all the same class, and phase 8 — the first non-trivial target — sits at the end. Only Phase 1 is quoted at $30,000; the cost of the remaining phases isn’t given.

The likely outcome is not that the pipeline fails — it’s that it doesn’t. Phases 1–7 would succeed, one after another, and the community would accumulate verified utility functions without ever reaching the hard target that justifies the programme.

I looked at the rust-lean repo to understand where the prior art stands. The Aeneas BasicProofs file is the interesting result — it shows the pipeline can extract production Rust (Result, Option, Usize, checked subtraction) and close 6 specifications against the extracted code. The four properties it proves are then imported into FoldingCorrectness.lean as axioms. The theorems stated in FoldingCorrectness.lean — polynomial degree reduction over a generic field, subdomain inclusion in the FRI tower — are well-formulated and non-trivial to even state correctly. But stated is not proved, and the harder proofs (currently sorry) seem to be beyond what AI can currently generate. The one theorem that currently crosses the bridge between extracted code and the independent spec is ⟨result, rfl⟩. Is this an acurate description of what you said?

So, is there a way to reshape this into something more useful for Zcash?

For example, is there a specific property in zebra-chain where you think the pipeline would genuinely add confidence that review and testing can’t — something with enough edge cases or subtlety that a proof would tell us something we don’t already know? If the pilot included one target at that level, even at small scope, it would demonstrate both the pipeline and its ceiling in a single phase.

[Natalie]

Thank you, I agree with most of what you say. Let me answer the three things that matter.

First, on the sorry stubs and whether this is beyond what AI can generate. Those stubs aren’t a ceiling, they’re where we stopped. That repo is a proof-of-concept: we were building and comparing the FV pipeline (Hax vs Aeneas extraction, the ArkLib bridge, Lean-specialized AI provers Aristotle and Aleph), and it was not about finishing every theorem.

On feasibility, here’s a concrete data point rather than a claim. The Polishchuk-Spielman lemma (a real coding-theory result, not a toy) was proved in Lean by Aleph, Logical Intelligence’s prover: 33 lemmas, 8.6 hours, about $215, merged in ArkLib #292 (same Verified-zkEVM org):

Proof of Polishchuk-Spielman (#292)

It needed hints and one statement-typo fix, so it wasn’t push-button, but it’s a genuinely complex proof produced by an AI prover and then cleaned up by engineers. We run Aleph and Aristotle (Harmonic) in our pipeline, not just general-purpose models.

Second, the more important point: you and Daira-Emma are converging. On the last Arborist Call she pointed me to crypto-related parsing as where bugs actually concentrate and where verification would add real value. That matches your EV argument, and it’s fair.

So here’s the reshaped scope: same pipeline, aimed at the crypto-object parsing layer, where length-check, canonical-encoding, point-on-curve and scalar-in-range bugs have historically concentrated in Zcash and Zcash-family chains. These are not omega targets, the work is harder:

• CompactSize parsing: round-trip plus canonical-encoding (non-minimal) rejection across all four bands (serialization/compact_size.rs). The canonicity half is the consensus-relevant, non-trivial part.
• Scalar-in-range parsing: Orchard Nullifier::try_from, and the Sapling and Orchard tree Root::try_from, accept iff the LE-encoded integer is strictly less than the curve order.
• Curve-point parsing with layered consensus checks: sapling::EphemeralPublicKey::try_from (canonical decode + not small-order) and orchard::EphemeralPublicKey::try_from (canonical decode + not identity). The point-on-curve check is enforced by the decoder itself; what we prove is the rejection logic layered on top.
• A targeted audit of the from_bytes(…).unwrap() sites in sapling/keys.rs (line 219 in TransmissionKey::try_from, line 358 in ValidatingKey::try_from), plus a cross-check that the small-order rejection in sapling EphemeralPublicKey and the identity rejection in orchard EphemeralPublicKey each match the corresponding consensus rule in the protocol spec.

These are targets where a proof tells you something review and testing don’t. The small-order vs identity asymmetry between the two EphemeralPublicKey paths is exactly the kind of subtle, consensus-relevant edge case that’s easy to miss by eye and that a proof pins down. To be clear about the boundary: we verify the parsing and validation layer here, length, canonicity, in-range, not the cryptography itself.

If this scope looks right, I’ll write up the full pilot proposal plus a follow-on roadmap for the rest of the parsing layer (Action composite parser, NoteCommitment / ValueCommitment, ValidatingKey, the Halo2Proof length cap, and other related entry points). @hanh what do you think about this new scope?

[hanh]

Thanks Natalie. This is a meaningful step forward from the initial scope. A few specifics:

On the reshaped scope: I agree the crypto object parsing layer is where bugs concentrate, and the examples you picked are the right ones. Those are CompactSize canonicity, scalar in range checks, and curve point decoding with layered rejection. That said, from a Lean proof perspective these all fall into the same narrow pattern: prove a function is injective over a domain defined by a range bound, a split, or a few case distinctions, then simp and omega close the rest. This is not a criticism. It just means the trial does not need to cover every variant to prove the approach works. One of these would be enough for a pilot. CompactSize is probably too simple to carry that weight. I would suggest the EphemeralPublicKey path instead, since it combines canonical decode with the small order or identity rejection logic, exactly the kind of layered consensus check that is subtle and worth pinning down. But really any single target from the list is acceptable as long as it demonstrates the pipeline end to end.

On translation: This is the critical point for me. When you say “extracted from Rust,” I need to know whether that means machine extraction or AI assisted translation. Machine extraction means a toolchain output with a fidelity argument, like Hax or Aeneas producing a Lean model that is provably equivalent to the Rust source. AI assisted translation means an AI reads the Rust and generates Lean, which has no formal connection to the Zebra codebase and adds little value beyond a standalone Lean exercise. If the pipeline is extraction based, the proposal should name the tool, the extraction boundary, and how the round trip fidelity argument works. If it is AI assisted, that should be explicit so we can weigh it accordingly. I think that’s not the case, but please let me know for sure.

Edit: The proposal mentions: “We apply our Rust → Aeneas → Lean 4 pipeline to the three target families described above (Amount, CompactSize64, Height). The Rust code is extracted into pure functional Lean 4, where we write formal specifications and prove correctness properties that the Lean kernel independently checks.”

On the trial and generality: If the translation mechanism is clarified and the scope is one well chosen target, a single trial is enough to show the pipeline holds up for this class of problem. But I want to be clear about what the trial does not demonstrate. CompactSize, scalar in range, and the curve point rejection logic all reduce to the same structural proof: injectivity over a bounded domain. A win there does not predict whether the approach scales to materially harder consensus properties, like signature verification, state machine invariants, or protocol level correctness of the Sapling or Orchard validation paths. I would like to know how you see this. Is the pitch that the tool delivers real value on the parsing layer and stops at that boundary? Or is the trial meant to de risk a broader formal verification program for Zebra? Either answer is fine. I just want us to be explicit about what is being claimed.

Happy to iterate once these points are nailed down, especially the extraction story.

[Natalie]

@hanh

materially harder consensus properties, like signature verification, state machine invariants, or protocol level correctness of the Sapling or Orchard validation paths.

Thanks! Answering the questions:

On extraction. Yes, it’s machine extraction, not AI translation. Charon lifts the Rust to LLBC, Aeneas produces a pure functional Lean 4 model from that. The Lean we prove against is toolchain output tied to the Rust source, not an AI’s reading of it. The AI provers (Aleph, Aristotle) operate only on the proof side, closing goals against that extracted model, and every proof they produce is kernel-checked. So the fidelity argument runs through Aeneas, and the AI never touches the code-to-Lean step. That distinction matters to us as much as to you (otherwise it’s not formal verification, it’s something else ).

On what the trial demonstrates, and what it doesn’t. You’re right that CompactSize, scalar-in-range, and the curve-point rejection all reduce to a similar structural shape. And a win there doesn’t predicts signature verification, state-machine invariants, or protocol-level correctness of the Sapling/Orchard validation paths. Those are a different order of difficulty. The honest reason is well known in the field: verification effort scales roughly with the square of the specification size (this is the seL4 experience, ~12 person-years for ~8.5k SLOC, ~200k lines of proof). That’s exactly why we don’t propose to boil the ocean The strategy is to verify small, high-value surfaces where the proof cost is bounded and the consequence of a bug is high.

So, to answer your either/or directly: it’s both, and I’ll say precisely what each part claims.

• The parsing layer has standalone value. Length, canonicity, in-range, and layered rejection checks are where consensus-relevant bugs have actually landed in Zcash-family code, and a proof closes those bug classes over all inputs. That value is real whether or not anything larger ever happens.
• The pilot also de-risks a larger program, but only for the parsing/validation layer, not for the hard consensus properties. It tells you the extraction and proof pipeline works end-to-end on real Zebra crypto-object code. It does not tell you we can verify the Orchard validation path. I’m not claiming it does.

On going further than parsing. To be clear, the parsing boundary is where this pilot stops, not where we stop. Materially harder targets, signature verification, state-machine invariants, protocol-level correctness of the validation paths, are things we do take on; our pipeline is already used on zkEVM cryptographic libraries under the Ethereum Foundation work, which is not an easy layer. Our company has around 25 senior engineers, with teams specialised in different verification approaches (interactive proof, SMT-backed methods, model checking), so the capability to go up the stack is there. But I’d want to earn each of those targets the same way we’re earning this one: pick one, scope it honestly, prove it, then decide the next. So yes, we can go further than the parsing layer, I’d just rather commit to it one de-risked step at a time than promise the whole stack up front.

By the way we’ve already run the pipeline end-to-end outside Zebra on Zooko’s smalloc allocator ( GitHub - runtimeverification/smalloc-verify: Formal verification of the pure-arithmetic kernel of [zooko/smalloc](https://github.com/zooko/smalloc) (`src/lib.rs`) · GitHub ), extraction through to kernel-checked proofs. So in this trial we are proving pipeline lands cleanly on Zebra’s actual crypto-parsing code and its dependencies, which is the part that’s genuinely Zebra-specific.

On the single target: agreed, one well-chosen target is enough, and EphemeralPublicKey is the right pick for the reason you gave, it’s the one that layers canonical decode with small-order / identity rejection rather than being a plain range check. We’re happy to start there.

On the trusted boundary. If that framing works for you, I’ll write up the pilot around EphemeralPublicKey (both the Sapling small-order and Orchard identity paths, since the asymmetry between them is the interesting part), with the rest of the parsing layer as an explicit follow-on program rather than bundled in.
One thing I want to be upfront about now rather than bury in the write-up: the trusted boundary. We prove that try_from accepts a 32-byte input iff it decodes canonically and passes the layered check, and that it never panics on any input. What we assume, as declared axioms, are the contracts of the underlying curve library: that jubjub/pallas from_bytes returns a point iff the encoding is canonical and on-curve, and that is_small_order / is_identity mean what they say. Closing that last gap would mean verifying the jubjub / pasta_curves crates themselves, which is a multi-month effort on its own and explicitly not in the pilot. The deliverable includes a written-out TCB so that line is visible, not hidden.

This is a small pilot by design, roughly one to two weeks of proof work once extraction infrastructure is in place, and I’ll put the exact scope, theorem list, and price in the full write-up. Before I do: does this division, standalone parsing value plus an explicit parsing-layer follow-on program, with the hard consensus properties and the curve-library internals both out of scope, match what you’d want to see in the proposal?

[hanh]

Thanks, I went ahead and looked at the smalloc allocator. That’s a single line of rust code, an arithmetic expression, without branching, error paths, etc. And so I am not sure it demonstrates more than the parsing, validation, range check. That’s fine. I think we are in agreement with what the rust to lean can do.
I’ll discuss more with the ZCG & ZF.

[Natalie]

Thanks, that’s fair on smalloc. I picked it cos Zooko had posted publicly that he’d been trying to formally verify that exact function and wanted to get a feel for the tooling, so I took it as a concrete request and turned it around in an afternoon.

EphemeralPublicKey is the deliberate step up from it, branching, error paths, layered rejection.

Glad we’re aligned on what the pipeline does. Appreciate you taking it to ZCG and ZF, and happy to write up the EphemeralPublicKey pilot as a concrete one-pager if that helps those discussions.

[ZCG]

Thank you for your submission. After consideration from ZCG and sufficient time for the community to provide feedback on the forum, the committee has decided to reject this proposal.

The committee appreciates your grant submission efforts and encourages you to continue as an active member of the Zcash community going forward!