Cryptography Track
Formalization of proof system specifications and verification of deployed implementations.
Overview
The work on this track has centered on three related libraries: ArkLib, a library formalizing executable specifications of SNARKs and unlderying mathematics (primarily coding theory); VCV-io, a library formalizing probabilistic computations and program logics for cryptographic games and security proofs; CompPoly, a library implementing computable polynomials, finite field arithmetic and evaluation algorithms which make ArkLib specifications executable.
Work on these libraries continues beyond this project, and form part of the stack used for the end-to-end specification of leanVM in Lean.
Verification Goals
Selected Resources
Grants
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
ArkLibRepositories
Verified-zkEVM/ArkLib
- Cryptography
Verified-zkEVM/VCVio
- Cryptography
Talks and Videos
September 2026
Gregor Mitscha-Baude - Ironwood
- Cryptography
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 · 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
March 2026
Manuel Puebla - AMO-Lean
- Cryptography
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
October 2025
Walkthrough of ArkLib
- Cryptography
March 2025
Q1 2025: Cryptography Track update
- Cryptography
Articles
January 2026 · zkSecurity
Lean4 Formalization of a Simplified Round-by-round Soundness Proof of FRI
- Cryptography