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.