Hi all,
I’ve opened a Pull Request to the Core-Grants repo with an RFC proposing formal verification of Kimchi and Pickles in Lean 4.
**Problem:** Kimchi’s PLONKish constraint system (15 columns, custom gates for foreign field arithmetic, Keccak, Poseidon, EC operations, Plookup) and Pickles’ recursive composition over the Pasta curve cycle are the cryptographic foundation of Mina’s constant-size blockchain. Their correctness has been established through audits and testing, but no machine-checked proofs exist. The deferred accumulator verification in Pickles is particularly subtle and would benefit from formal analysis.
**Proposal:** Build the first formal model of Kimchi/Pickles in Lean 4, targeting five areas: (1) custom gate soundness, (2) Plookup argument correctness, (3) Pickles recursive composition, (4) Fiat-Shamir transcript binding, and (5) Pasta curve arithmetic. All artifacts open-sourced.
**Scope:** 12 months, $96,000 ($8,000/month), independent researcher.
**Background:** PhD Mathematics, career software engineer, production Rust/WASM. Currently pursuing formal verification of ZK proof systems across multiple ecosystems (pending grants with Zcash Community Grants and Ethereum Foundation ESP for Halo 2 and EVM verification respectively).
Seeking community feedback on scope, priorities, and any technical considerations I should address. Happy to answer questions.