Resources
Repositories
Verified-zkEVM
GitHub organization
Verified-zkEVM/evm-asm
Verified macro assembler building the EVM guest bottom-up from a machine-checked RV64 core (experimental prototype)
- EVM
Verified-zkEVM/ArkLib
- Cryptography
Verified-zkEVM/CompPoly
- EVM
Verified-zkEVM/iris-lean
- EVM
Verified-zkEVM/VCVio
- Cryptography
Verified-zkEVM/clean
- zkVM
Verified-zkEVM/ExtTreeMapLemmas
- General
Verified-zkEVM/leanerVM
Verified-zkEVM/PolyFun
- General
Verified-zkEVM/riscv-zkvm
- zkVM
Verified-zkEVM/rust-lean
- General
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/.github
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
opencompl/veir
Compiler infrastructure in Lean with MLIR interoperability.
- General
Veridise/zirgen-to-llzk
- zkVM
NethermindEth/CertiPlonk
- zkVM
pirapira/stateless-pancaketh
Experimental Ethereum stateless guest implementation in Pancake.
- EVM
formal-land/garden
- zkVM
Talks and Videos
September 2026
Devon Tuma - Verifying SP1 constraints with clean
- zkVM
September 2026
Gregor Mitscha-Baude - Ironwood
- Cryptography
August 2026
Giorgio Dell'Immagine - zkGolf
- zkVM
August 2026 · SBC 2026
Alexander Hicks - AI vs QED: formally verifying the stack
- General
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
Mathieu Fehr - Formal Semantics for MLIR dialects
- General
May 2026 · ZKProof 8
Quang Dao - Evolving the foundations of ArkLib
- Cryptography
May 2026 · ZKProof 8
Julian Sutherland - Reasoning about IOPPs
- Cryptography
May 2026 · ZKProof 8
Katerina Hristova - Mathematical foundations
- Cryptography
May 2026 · ZKProof 8
Derek Sorensen - CompPoly
- Cryptography
May 2026 · ZKProof 8
Devon Tuma - VCVio
- Cryptography
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
May 2026 · Lean FRO
Bas Spitters - Software Verification in Lean
- Cryptography
May 2026 · Lean FRO
Quang Dao - Software Verification in Lean
- Cryptography
April 2026
Yoichi Hirai - Your guide to formal verification when machines write Lean proofs
- Cryptography
April 2026
Derek Sorensen - Safely Snarkifying Ethereum: Formal Verification and Protocol
- Cryptography
April 2026
Luisa Cicolini - Certified Instruction Selection For LLVM IR Through Bitblasting
- General
April 2026
Petar Maksimović - OpenVM and Pico in Lean
- zkVM
March 2026
Manuel Puebla - AMO-Lean
- Cryptography
March 2026
Eske Nielsen - Peregrine
- zkVM
February 2026
Bas Spitters - SSProve-Lean
- Cryptography
February 2026
Julian Sutherland - FRI in ArkLib + Yoichi Hirai - Vibe FRI RBR soundness
- Cryptography
January 2026
Coding Theory in ArkLib
- Cryptography
January 2026
ArkLib
- Cryptography
December 2025
Formally Verifying the SP1 RISC-V AIRs
- zkVM
November 2025
Securing Ethereum: The ZK-EVM Formal Verification Project
October 2025
Walkthrough of ArkLib
- Cryptography
October 2025
Elizaveta Pertseva - Automated Lean Proofs for Every Type
- zkVM
October 2025
pq2-05: e2e Formal Verification
- EVM
October 2025
Comparing ZK Constraints - Keccak, Plonky3 - Rust/Rocq
- EVM
- zkVM
September 2025
LLZK: Open-source infrastructure for secure ZK
- zkVM
March 2025
Formally verifying zk(E)VMs with the Ethereum Foundation
March 2025
Towards a verified Jolt zkVM
- zkVM
March 2025
Q1 2025: Cryptography Track update
- Cryptography
March 2025
Q1 2025: zkVM Track update
- zkVM
March 2025
Q1 2025: EVM Track update
- EVM
Papers
Papers may be co-funded with other organizations, and not all authors are necessarily funded by this project.
OOPSLA 2025
Certified Decision Procedures for Width-Independent Bitvector Predicates
Siddharth Bhat, Léo Stefanesco, Chris Hughes, Tobias Grosser.
- EVM
OOPSLA 2025
Interactive Bitvector Reasoning using Verified Bit-Blasting
Henrik Böving, Siddharth Bhat, Luisa Cicolini, Alex Keizer, Léon Frenot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark Barrett, Tobias Grosser.
- EVM
Articles
April 2026 · zkSecurity
The Final Form of Software Development
- General
January 2026 · zkSecurity
Lean4 Formalization of a Simplified Round-by-round Soundness Proof of FRI
- Cryptography
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