Grants
Grant applications are closed. No new proposals are being accepted. This page preserves the application guidelines for reference and the full record of awarded work.
Requests for Proposals
There are no active requests for proposals.
Application Guidelines (Archived)
These guidelines describe the requirements used when applications were open. They are retained for reference; new proposals are not being accepted.
Applications required a written proposal in PDF format addressing the following details:
-
Proposal overview
-
Proposed work, including goals, approach, and expected outcomes. Proposals should clearly explain what the proposal's target is and what a successful completion of the work would enable.
-
Chosen methods and tools.
-
Challenges, risks, and expected caveats.
-
Timeline, including possible milestones. Do you need some other work to be completed (by yourself or others) before beginning your proposed work?
-
Team composition.
-
Costs.
-
-
Technical approach
-
Breakdown of technical tasks.
-
References to relevant work.
-
-
Project management
-
Plans for coordination and communication about your work.
-
Approach to maintaining or extending your work and enabling external contributions to facilitate this.
-
Planned resource allocation (human and financial).
-
-
Team
-
Background and expertise of your team members.
-
Track record, including public repositories and published work relevant to your proposal.
-
Applications were open to individuals, teams, and organizations, with funding selected on a case-by-case basis. Applicants could submit more than one proposal as long as each proposal was distinct and relevant to the project. Funding was subject to a KYC process.
Several independent proposals could have similar goals. In such cases, several proposals could be funded if comparing the results of different approaches to the same problem would be useful, or if several teams could work together on similar or complementary goals. Flexibility in this regard was encouraged.
Proposals for general tooling were expected to explain how the tooling would be useful within the expected lifetime of this project (e.g., verifying a specific artefact) and how others could also use it.
Applications related to the cryptography track were expected to take into account ArkLib.
Applications related to circuits were expected to take into account LLZK.
Awarded Grants
zkVM Track
OpenVM Formal Verification
Intended to support formal verification of OpenVM’s RISC-V constraints against the official Sail semantics in Lean.
Awarded to: Axiom
openvm-fvFormal Verification of the Brevis Pico RISC-V zkVM
Intended to support formal verification of Brevis Pico’s RISC-V constraints against the official Sail semantics in Lean.
Awarded to: Nethermind
pico-fvGPU-Accelerated R1CS Witness Generation for LLZK
Intended to support GPU-accelerated R1CS witness generation for LLZK using an MLIR-based compiler stack.
Awarded to: Fractalyze
llzk-to-shloImproved Proving Infrastructure for RISC-V zkVMs
Intended to support Lean infrastructure for verifying SP1’s RISC-V constraints against the official Sail semantics.
Awarded to: SP1, Nethermind
sp1-leanNoir to LLZK compiler
Intended to support the development of a compiler from Noir to LLZK via ACIR.
Awarded to: Rei Labs
noir_llzkVerifying autoprecompiles
Intended to support the verification of Powdr Labs' autoprecompiles.
Awarded to: Powdr Labs GmbH, Certora
AVAZAR: Automatic verification tools for zkVM arithmetization
Intended to support work on automated verification tools for zkVM arithmetizations.
Awarded to: Universidad Complutense de Madrid (Albert Rubio)
AVAZARZKVM Agnostic Fuzzing
Intended to support the development of fuzzing techniques applicable to any RISC-V zkVM.
Awarded to: zksecurity
zkvmblastzkBugs 2.0
Intended to support an update of zkBugs.
Awarded to: zksecurity
Automated Verification of ZK Circuits
Intended to support the development of techniques to automatically verify the consistency between witness generation and constraints.
Awarded to: Veridise
LLEQZKarnage: Stress Testing ZK Systems Through Maximum Pain
Intended to support work on prover killers.
Awarded to: Conner Swann
ZKarnagePlonky3 in Rocq
Intended to support an integration of Plonky3 with Rocq.
Awarded to: Formal Land
GardenPlonky3 to Lean
Intended to support an integration of Plonky3 with Lean.
Awarded to: Nethermind
CertiPlonkEvaluating Verus for circuits and EVM precompiles
Intended to support an evaluation of Verus as a tool to verify representative Rust code.
Awarded to: CertiK
zkvm-verusBetter Rocq tactics for modular arithmetic & handling packed integers
Intended to support the development of Rocq tactics for handling arithmetic modulo and packed integers.
Awarded to: CertiK
rocq_zkvm_tacticscLean
Intended to support the development of a Lean DSL aimed at writing AIR circuits directly in Lean.
Awarded to: zkSecurity
RepositoryLLZK
Intended to support the development of LLZK, a family of MLIR dialects for circuits.
Awarded to: Veridise
llzk-libLean backend for Sail
Intended to support a Lean backend for Sail so that the official RISC-V Sail specification can be extracted to Lean.
zkLean
Intended to support a Lean DSL for constraints and its integration with LLZK.
Awarded to: Galois
zkLeanEVM Track
evm-asm
Intended to support the development of formally verified Ethereum execution guest programs for zkVMs, exploring macro assembly in Lean and verified compilation.
Awarded to: zkSecurity
Certified compilation
Intended to support research on certified compilation methods in the Rocq ecosystem together with tools for high-assurance cryptography.
Awarded to: Aarhus University
Development of an EVM in Rocq
Intended to support the development of a canonical, maintainable, and validated EVM specification in Rocq.
Awarded to: KTH Royal Institute of Technology
Verification of revm and Lean backend for K
Intended to support verification of revm compiled to RISC-V against KEVM together with development of a Lean backend for K.
Awarded to: Runtime Verification
Cryptography Track
The recursive extraction problem
Intended to support research on the recursive extraction problem in proof systems.
Awarded to: Cornell University
Formalising proximity generators
Intended to support the formalization of proximity generators and related properties in ArkLib.
Awarded to: Katerina Hristova
ArkLibCompPoly P2 roadmap
Intended to support Phase 2 of CompPoly’s roadmap, including fast field arithmetic, polynomial operations, exponentiation, multilinear transforms, and error-correcting interpolation.
Awarded to: Formal Land, zkSecurity, Dimitris Mitsios, Runtime Verification
CompPolyProtocol IR
Intended to support the development of an intermediate representation and compiler for zero-knowledge protocols, enabling protocol checks, generation of prover and verifier programs, and security analysis.
Awarded to: Wonjae Choi
zkcRust Verification Through Lean 4 Tooling
Intended to support investigation into Lean 4 based formal verification of Rust components used in zkEVM and zkVM stacks.
Awarded to: Runtime Verification
rust-leanSTIR & WHIR constructions in ArkLib
Intended to support the addition of executable specifications for STIR and WHIR in ArkLib.
Awarded to: Nethermind
ArkLibFiat-Shamir specification and review
Intended to support the development, formal verification, and technical review of a Fiat-Shamir specification based on duplex sponges.
Awarded to: Article 12, LLC (Michele Orrù), Alessandro Chiesa, Chung Thai Nguyen
ArkLibBluebell
Intended to support implementation of the Bluebell program logic in Lean for use in ArkLib.
Awarded to: Nethermind
iris-leanAI proofs in ArkLib
Intended to support experiments in using Logical Intelligence's AI tools for proofs in ArkLib.
Awarded to: Logical Intelligence
ArkLibBinius in ArkLib
Intended to support the formalization of Binius in ArkLib.
Awarded to: Chung Thai Nguyen
ArkLibBlueprint STIR and WHIR in ArkLib
Intended to support development of a blueprint for STIR and WHIR security theorems in ArkLib.
Awarded to: Least Authority
ArkLibBlueprint for FRI & Coding Theory prerequisites in ArkLib
Intended to support development of a blueprint for FRI and coding theory prerequisites in ArkLib.
Awarded to: Nethermind
ArkLibArkLib
Intended to support development of ArkLib, a library of formalized proof systems in Lean, together with work on VCVio.
Awarded to: Quang Dao, Devon Tuma, zkSecurity
ArkLibGeneral Tooling
Events
HACS
Support for the High Assurance Crypto Software workshops in 2025 and 2026.
ZKProof events
Support for the ZKProof Zurich event, ZKProof 7, and the Verified zkEVM ArkLib Day at ZKProof 8.
Awarded to: ZKProofs
Community Resources and Education
Foundations of Probabilistic Proofs MOOC
Intended to support development of a MOOC on the foundations of probabilistic proofs.
Awarded to: Algorithmic Security GmbH (Alessandro Chiesa)
EthProofs
Intended to support continued development of ethproofs.org.
Awarded to: Fara Woolf
EthProofs