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:

  1. 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.

  2. Technical approach

    • Breakdown of technical tasks.

    • References to relevant work.

  3. 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).

  4. 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

Verifying autoprecompiles

Q4 2025

Intended to support the verification of Powdr Labs' autoprecompiles.

Awarded to: Powdr Labs GmbH, Certora

AVAZAR: Automatic verification tools for zkVM arithmetization

Q4 2025

Intended to support work on automated verification tools for zkVM arithmetizations.

Awarded to: Universidad Complutense de Madrid (Albert Rubio)

ZKVM Agnostic Fuzzing

Q3 2025

Intended to support the development of fuzzing techniques applicable to any RISC-V zkVM.

Awarded to: zksecurity

zkBugs 2.0

Q3 2025

Intended to support an update of zkBugs.

Awarded to: zksecurity

zkBugs

Automated Verification of ZK Circuits

Q3 2025

Intended to support the development of techniques to automatically verify the consistency between witness generation and constraints.

Awarded to: Veridise

ZKarnage: Stress Testing ZK Systems Through Maximum Pain

Q2 2025

Intended to support work on prover killers.

Awarded to: Conner Swann

Plonky3 in Rocq

Q2 2025

Intended to support an integration of Plonky3 with Rocq.

Awarded to: Formal Land

Plonky3 to Lean

Q1 2025

Intended to support an integration of Plonky3 with Lean.

Awarded to: Nethermind

Evaluating Verus for circuits and EVM precompiles

Q1 2025

Intended to support an evaluation of Verus as a tool to verify representative Rust code.

Awarded to: CertiK

Better Rocq tactics for modular arithmetic & handling packed integers

Q1 2025

Intended to support the development of Rocq tactics for handling arithmetic modulo and packed integers.

Awarded to: CertiK

cLean

Q4 2025

Intended to support the development of a Lean DSL aimed at writing AIR circuits directly in Lean.

Awarded to: zkSecurity

Repository

LLZK

Q4 2024, Q4 2025

Intended to support the development of LLZK, a family of MLIR dialects for circuits.

Awarded to: Veridise

Lean backend for Sail

Q1 2025, Q3 2025

Intended to support a Lean backend for Sail so that the official RISC-V Sail specification can be extracted to Lean.

Awarded to: University of Cambridge, Galois, Lindy Labs (first grant only)

zkLean

Q1 2025, Q3 2025

Intended to support a Lean DSL for constraints and its integration with LLZK.

Awarded to: Galois

EVM Track

Certified compilation

Q4 2024

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

Q4 2024

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

Q4 2024

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

Technical Review of Fiat-Shamir From Duplex Sponges

Q4 2025

Intended to support a technical review of the Fiat-Shamir transformation instantiated via duplex sponges.

Awarded to: University of Maryland (Kasra Abbaszadeh)

Rust Verification Through Lean 4 Tooling

Q4 2025

Intended to support investigation into Lean 4 based formal verification of Rust components used in zkEVM and zkVM stacks.

Awarded to: Runtime Verification

STIR & WHIR constructions in ArkLib

Q4 2025

Intended to support the addition of executable specifications for STIR and WHIR in ArkLib.

Awarded to: Nethermind

Fiat-Shamir specification

Q4 2025

Intended to support the development of a Fiat-Shamir specification based on duplex sponges.

Awarded to: Article 12, LLC (Michele OrrĂ¹)

Bluebell

Q3 2025

Intended to support implementation of the Bluebell program logic in Lean for use in ArkLib.

Awarded to: Nethermind

AI proofs in ArkLib

Q3 2025

Intended to support experiments in using Logical Intelligence's AI tools for proofs in ArkLib.

Awarded to: Logical Intelligence

Binius in ArkLib

Intended to support the formalization of Binius in ArkLib.

Awarded to: Chung Thai Nguyen

Blueprint STIR and WHIR in ArkLib

Q1 2025

Intended to support development of a blueprint for STIR and WHIR security theorems in ArkLib.

Awarded to: Least Authority

Blueprint for FRI & Coding Theory prerequisites in ArkLib

Q1 2025

Intended to support development of a blueprint for FRI and coding theory prerequisites in ArkLib.

Awarded to: Nethermind

ArkLib

Q4 2024

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

ArkLib

General Tooling

MLIR sidekick for Lean

Q3 2025

Intended to support Lean-MLIR infrastructure development, including fast datastructures and a RISC-V dialect in Lean.

Awarded to: University of Cambridge

Lean backend for hax

Q2 2025, Q4 2025

Intended to support development of a Lean backend for hax.

Awarded to: Cryspen

hax

Events

HACS 2026

Q1 2026

Support for HACS 2026 in March 2026.

Awarded to: Aspiration

Overview

HACS 2025

Q1 2025

Support for HACS 2025 in March 2025.

Awarded to: Aspiration

Overview

ZKProofs 7

Q1 2025

Support for ZKProofs 7 in March 2025.

Awarded to: ZKProofs

Event

ZKProofs Zurich Event

Q4 2024

Support for a Zurich event discussing the formal verification of proof systems.

Awarded to: ZKProofs

Summary

Community Resources and Education

Foundations of Probabilistic Proofs MOOC

Q3 2025

Intended to support development of a MOOC on the foundations of probabilistic proofs.

Awarded to: Algorithmic Security GmbH (Alessandro Chiesa)

EthProofs

Q2 2025, Q3 2025

Intended to support continued development of ethproofs.org.

Awarded to: Fara Woolf