zkVM Track
Verification of zkVM constraints against the official RISC-V Sail semantics.
Overview
The work on this track included the development of a general purpose Lean backend for Sail, which was subsequently used to verify RISC-V zkVM chips. Concurrent work on this track also served to establish clean, a Lean DSL for constraints, which has been successfully used as an extraction target for constraints generated in Rust and the development of verified constraints and witness generation logic natively verified in Lean. LLZK, a MLIR based compiler toolchain, was also developed as part of the work om this track, supporting the use of SMT based verification tools on a greater number of frontends, and paving the way for a verified compiler toolchain via VeIR.
Verification Goals
Selected Resources
Grants
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
zkLeanRepositories
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