Cryptography Track
Verification of proof systems, security arguments, and cryptographic components used by zkVMs and zkEVMs.
Overview
Verification Goals
Selected Resources
Grants
Technical Review of Fiat-Shamir From Duplex Sponges
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
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
Intended to support the addition of executable specifications for STIR and WHIR in ArkLib.
Awarded to: Nethermind
Fiat-Shamir specification
Intended to support the development of a Fiat-Shamir specification based on duplex sponges.
Awarded to: Article 12, LLC (Michele Orrù)
Bluebell
Intended to support implementation of the Bluebell program logic in Lean for use in ArkLib.
Awarded to: Nethermind
AI proofs in ArkLib
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
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
Intended to support development of a blueprint for FRI and coding theory prerequisites in ArkLib.
Awarded to: Nethermind
ArkLib
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