zkVM Track
Verification of zkVM arithmetizations against the official RISC-V Sail semantics.
Overview
Verification Goals
Selected Resources
Grants
Verifying 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)
ZKVM Agnostic Fuzzing
Intended to support the development of fuzzing techniques applicable to any RISC-V zkVM.
Awarded to: zksecurity
zkBugs 2.0
Intended to support an update of zkBugs.
Awarded to: zksecurity
zkBugsAutomated Verification of ZK Circuits
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
Intended to support work on prover killers.
Awarded to: Conner Swann
Plonky3 in Rocq
Intended to support an integration of Plonky3 with Rocq.
Awarded to: Formal Land
Plonky3 to Lean
Intended to support an integration of Plonky3 with Lean.
Awarded to: Nethermind
Evaluating Verus for circuits and EVM precompiles
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
Intended to support the development of Rocq tactics for handling arithmetic modulo and packed integers.
Awarded to: CertiK
cLean
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
Lean backend for Sail
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
Intended to support a Lean DSL for constraints and its integration with LLZK.
Awarded to: Galois
Repositories
Verified-zkEVM/clean
- zkVM
Verified-zkEVM/riscv-zkvm
- zkVM
Verified-zkEVM/zkLean
- zkVM
project-llzk/circom
- zkVM
project-llzk/llzk-lib
- zkVM
project-llzk/llzk-rs
- zkVM
project-llzk/llzk-nix-pkgs
- zkVM
project-llzk/llzk-benchmarks
- zkVM
project-llzk/airbender-llzk-frontend
- zkVM
project-llzk/circom-benchmarks
- zkVM
project-llzk/clean-llzk-frontend
- zkVM
project-llzk/haloumi
- zkVM
project-llzk/LLEQ
- zkVM
project-llzk/llzk-interpreter
- zkVM
project-llzk/llzk-lean
- zkVM
project-llzk/llzk-spec
- zkVM
project-llzk/noir-benchmarks
- zkVM
project-llzk/noir_llzk
- zkVM
Veridise/zirgen-to-llzk
- zkVM
NethermindEth/CertiPlonk
- zkVM
formal-land/garden
- zkVM
Talks and Videos
September 2026
Devon Tuma - Verifying SP1 constraints with clean
- zkVM
August 2026
Giorgio Dell'Immagine - zkGolf
- zkVM
June 2026
Raghav Malik - LLZK equivalence checker
- zkVM
June 2026
Ian Neal & Daniel Dominguez Alvarez - LLZK verification dialect
- zkVM
June 2026
Ryan Kim - A Verifiable ZK Compiler Stack for Lean
- zkVM
May 2026
Ian Neal & Timothy Hoffman - LLZK 1.0
- zkVM
May 2026 · ZKProof 8
James Parker - zkLean: A DSL for ZK statement verification
- zkVM
May 2026 · ZKProof 8
Gregor Mitscha-Baude - Clean: From verification of circuits to verification of zkVMs
- zkVM
April 2026
Petar Maksimović - OpenVM and Pico in Lean
- zkVM
March 2026
Eske Nielsen - Peregrine
- zkVM
December 2025
Formally Verifying the SP1 RISC-V AIRs
- zkVM
October 2025
Elizaveta Pertseva - Automated Lean Proofs for Every Type
- zkVM
October 2025
Comparing ZK Constraints - Keccak, Plonky3 - Rust/Rocq
- EVM
- zkVM
September 2025
LLZK: Open-source infrastructure for secure ZK
- zkVM
March 2025
Towards a verified Jolt zkVM
- zkVM
March 2025
Q1 2025: zkVM Track update
- zkVM
Articles
January 2026 · Formal Land
Formal verification of the Keccak precompile from Plonky3
- EVM
- zkVM
November 2025 · zkSecurity
Comparison of Formal Verification Frameworks for Arithmetic Circuits
- zkVM
November 2025 · Nethermind
Formally Verifying Zero-Knowledge Circuits: Introducing CertiPlonk
- zkVM
September 2025 · Formal Land
Verification of the completeness of an OpenVM chip
- zkVM
August 2025 · Veridise
Announcing LLZK: A unified, open-source intermediate representation for zero-knowledge languages
- zkVM
August 2025 · Formal Land
Pretty-printing of Rust ZK constraints
- zkVM
August 2025 · Formal Land
Formal verification of an OpenVM chip
- zkVM
July 2025 · Formal Land
Formal verification of LLZK circuits in Rocq
- zkVM
July 2025 · Formal Land
Semantics for LLZK in Rocq
- zkVM
July 2025 · Formal Land
Beginning of a formal verification tool for LLZK
- zkVM
June 2025 · Formal Land
Beginning of translation of OpenVM to Rocq
- zkVM
March 2025 · zkSecurity
Introducing clean, a formal verification DSL for ZK circuits in Lean4
- zkVM