Hello everyone,
I’m submitting a proposal on behalf of Runtime Verification to formally verify Zcash’s CompactSize variable-length integer encoding using our Rust → Aeneas → Lean 4 pipeline, producing machine-checked proofs of five consensus-critical correctness properties.
Why This Matters
CompactSize is the Bitcoin-derived encoding used throughout Zcash transaction serialization: input/output counts, vector lengths, field sizes. Every transaction parse and serialize path goes through it. A bug here, particularly a canonicity violation, could result in two nodes interpreting the same byte sequence differently and cause a consensus split. Non-minimal encodings have previously been identified as a potential vulnerability in the Zcash codebase (zcash/zcash#842).
Formal verification is particularly important now that AI is being actively used to find vulnerabilities in production codebases: machine-checked proofs eliminate entire classes of bugs permanently, which is especially valuable for consensus-critical functions like transaction serialization.
What We Will Prove
We will formally prove five properties of the CompactSize implementation: that parsing is the inverse of serialization (round-trip), that non-minimal encodings are rejected (canonicity), that parsing never panics on malformed input (panic-freedom), that parsing consumes at most 9 bytes regardless of input (bounded reads), and that no two distinct values produce the same byte sequence (injectivity).
Our Pipeline
RV has established and validated a formal verification pipeline integrating Charon, Aeneas, and Lean 4. We have successfully applied it to FRI polynomial-folding primitives from Plonky3 and Mersenne31 prime field arithmetic, as demonstrated in Verified-zkEVM/rust-lean and through upstream Aeneas contributions #832 and #833. On the proving side, we additionally leverage AI-assisted proof tools, where applicable, to make the verification process faster and more tractable.
CompactSize is a well-matched target: the core encoding logic is roughly 80 lines of pure Rust with no unsafe code, no async, and no concurrency. We have already run an initial proof-of-concept extraction and identified the key technical challenges and how we will address them.
Deliverables
All proof artifacts will be published in a public repository with CI that rebuilds the proofs on every commit. The deliverables include a standalone Rust extraction target, the Aeneas-extracted Lean 4 translation, a formal specification of all five properties, machine-checked proofs with no sorry, and a final report documenting the pipeline, theorem list, build instructions, and any limitations encountered.
Collaboration
We see this work as complementary to other formal verification efforts emerging in the Zcash ecosystem, and are actively open to collaborating with contributors and maintainers who share an interest in building out verification infrastructure for Zcash. We are also happy to present our pipeline and proposed approach to the community and development team, whether in a community call, an Arborist call, or any other forum, if it helps.
Budget and Timeline
$80,000 over 4 weeks, structured as:
-
$20,000 startup
-
$20,000 at milestone 1 (end of week 2): extracted model + spec + proofs of properties 1 & 3
-
$40,000 at milestone 2 (end of week 4): all five proofs + final report + public CI repo
Full proposal details are available here: ZcashCommunityGrants/zcashcommunitygrants#278
We welcome community feedback and questions.