ArkLib: Lean 4 library for verifying SNARK components: IORs, sum-check, FRI, STIR, WHIR, Fiat-Shamir
================================================================================

ArkLib formalizes the building blocks of modern SNARKs in Lean 4: interactive oracle reductions and their composition, sum-check, polynomial commitment schemes, the FRI, STIR and WHIR proximity protocols, Fiat-Shamir and the BCS transform, with completeness and soundness theorems. It is the proof-system half of the Verified zkEVM program.

Maintainer: Verified-zkEVM (Quang Dao et al., Ethereum Foundation)
Website: https://github.com/Verified-zkEVM/ArkLib
Category: Proof systems and computational proofs
Targets: Interactive oracle reductions, Sum-check, Polynomial commitments, FRI / STIR / WHIR, Fiat-Shamir, BCS
Approach: Lean 4 with VCV-io for probabilistic reasoning; completeness and soundness of proof-system components
Access: Open source
Status: Active; Nethermind maintains an ArkLibFri fork
Strengths: Only library formalizing the actual proof-system components used in production zkEVMs. | Lean 4, composable with Clean and other circuit proofs. | Backed by the EF and Nethermind.
Limits: Research-shaped; APIs and coverage change quickly. | Requires deep familiarity with both Lean and proof-system theory. | Not a tool you point at a codebase.
Firms using it: Nethermind (Formal Verification team)
Sources: https://github.com/Verified-zkEVM/ArkLib | https://blog.ethereum.org/2025/12/18/zkevm-security-foundations | https://verified-zkevm.org

Source page: https://sorryfree.com/frameworks/arklib/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13