https://github.com/ZcashCommunityGrants/zcashcommunitygrants/issues/438
Requested Grant Amount (USD):
$8000
Category
Security
Project Lead
Name: Ariel Gabizon
Role: Researcher/Cryptographer
Background: Worked on snarks and Zcash for many years
Project Summary
Ironwood has recently been formally verified. We want a human readable math paper describing the lean proof.
Project Description
As said above, the ultimate goal is a human readable math paper following the Ironwood formal verification lean code. Here we propose a modest first but interesting step:
The FV code contains a proof of the bulletproofs protocols using the Algebraic Group Model that is much simpler than proofs in the literature. It is skteched here in the Inner Product Arguments section:
https://tachyon.z.cash/blog/ironwood-verification-complete
We wish to write a short (6-8) page note formally describing this proof.
Beyond helping understand and secure Irownwood, exposition of this simpler proof would be a contribution to the academic community.
Proposed Problem
After the counterfeiting bug discovered by Taylor Hornby, Zcash migrated to Ironwood, for
which it formally verified soundness. This was an impressive undertaking resulting in Zcash’s security measures adhering to a new high standard for other blockchain and zero-knowledge projects to follow.
However, it is important for humans to understand what the formal statement being proven are - as to gauge if what is being formally verified captures real world security and attacks. More generally, it is risky to reach a point where humans (in the sense of some non-empty subset of humans, potentially of size one 
) no longer understand the math on which the security of the systems they rely on on is based.
Proposed Solution
To aid in this, we propose a human written and readable math paper describing the statements and proofs in the Irownwood FV.
We stress again that this small grant proposal is about just one component in this paper - the new simplified proof of the bulletproofs protocol (a core component in Zcash’s SNARK).
Startup Funding (USD)
8000
Startup Funding Justification
Would be nice to get the funding in advance, but not essential
Milestone Details-
Milestone: 1
Amount (USD): 8000
Expected Completion Date: 2026-11-1
Deliverables:
- A PDF titled “A simplified bulletproofs security proof based on the Zcash Ironwood formal verification”