Hi artkor, thank you for the thoughtful questions. I am happy to address each.
1. Background and motivation
My PhD thesis is from 2010 and was indeed in applied mathematics (mathematical biology). That was 16 years ago. In the time since, my career has been in software engineering, with the last several years focused specifically on Rust in the blockchain space, and my very recent work involving cryptographic protocols and formal verification.
Some concrete recent work that is more relevant than the thesis:
-
I have been an active security researcher across ZK and DeFi protocols, including bounty programs on PancakeSwap, Euler, Hyperliquid, and LayerZero, with confirmed findings involving smart contract analysis and protocol-level reasoning.
-
I have contributed to GitHub - GaloisInc/cryptol: Cryptol: The Language of Cryptography · GitHub , Galois’s domain-specific language for cryptographic algorithm specification, including implementing a DIMACS SAT adapter and a :count command for model counting (sharpSAT integration). Cryptol is used by the NSA and DARPA for crypto specification work.
-
Most directly relevant: I have already completed the LookupRangeCheck formalization in Lean 4 ( GitHub - MavenRain/halo2-formal · GitHub ) before requesting any funding. This is 244 lines of Lean 4 with soundness and completeness proofs grounded in Mathlib, covering the running-sum range check, the short range check, and the no-wrap guarantee for the Pallas field. It demonstrates the exact methodology that carries through to the remaining gadgets.
What drew me to Halo 2 specifically: the Zcash Orchard circuit is one of the more consequential deployed ZK systems (it protects real user funds and privacy), it has mature public specifications (ZIP 224, the Orchard book, the Halo 2 book), and Nethermind’s Halva framework proved the viability of extracting Halo 2 constraints into Lean 4, including discovering a severe soundness bug in Scroll’s Keccak circuit using this approach. Zcash’s own gadgets have not received this treatment yet, and the methodology is a natural fit for my current interests and skills.
2. Project framing
This is Zcash-specific work, not general Halo research. Every deliverable targets Zcash’s actual deployed Orchard circuit.
Concretely:
-
Phase 1 produces Lean 4 proofs that Zcash’s five Orchard gadgets (Sinsemilla, Poseidon/Pow5, ECC, MerklePath, LookupRangeCheck) correctly enforce the intended computation. If a constraint in the production circuit is unsound, these proofs will surface it. Over 80% of findings in ZK audit reports trace back to the circuit layer, and manual audits cannot provide completeness guarantees.
-
Phase 2 lifts this to the protocol layer, proving that Orchard (ZIP 224) achieves spend authorization, balance, and Fiat-Shamir soundness when instantiated with the verified circuits.
Practical example: Nethermind used Halva (the same framework I build on) to discover that Scroll’s deployed Keccak-256 circuit had a soundness bug, meaning an attacker could have produced accepting proofs for incorrect hash outputs. This class of vulnerability is exactly what formal verification catches and manual audit misses. My work would provide that assurance for Zcash’s own circuits.
3. Protocol team interaction
Minimal. The core inputs to this work are all public:
-
The Halo 2 Rust crates (zcash/halo2, zcash/orchard) on GitHub
-
The Halo 2 book and Orchard book
-
ZIP 224 specification
-
Nethermind’s open-source Halva framework
I do not anticipate needing substantial protocol team involvement. The work is self-contained: read the public code and specs, extract constraints into Lean 4, prove properties. If ambiguities arise in the specification, I would ask targeted questions (in a forum post, for example), but nothing that would consume ongoing specialist time.
The proposal is also structured to protect against overcommitment: milestone-gated payments, a scope-down option (Phase 1 only at $67,200 over 4 months), and the fact that one gadget is already done before any funding has been requested.
I hope this helps. Let me know if you have any further questions!
