ArkLib
Direct answerArkLib 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
- Repository
- https://github.com/Verified-zkEVM/ArkLib
- Category
- Proof systems and computational proofs
- Targets
- Interactive oracle reductionsSum-checkPolynomial commitmentsFRI / STIR / WHIRFiat-ShamirBCS
- Approach
- Lean 4 with VCV-io for probabilistic reasoning; completeness and soundness of proof-system components
- Access
- Open source
- Status (2026-09-13)
- Active; Nethermind maintains an ArkLibFri fork
What ArkLib does
The Ethereum Foundation's December 2025 roadmap requires a formal soundness argument for recursion by the end of 2026; ArkLib is the vehicle. Its FRI work is also where the better.codes proximity bound feeds in, since the provable soundness of hash-based SNARKs depends on Reed-Solomon proximity results.
Where it is strong
- 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 and caveats
- 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.
When to choose it
Engage with ArkLib if you build a proof system or need a machine-checked soundness bound for recursion or a proximity protocol.
Who works with ArkLib
Nethermind (Formal Verification team).
Top-listed for proof-system verification work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Related frameworks in Proof systems and computational proofs
EasyCrypt, CryptoVerif, SSProve, ProofFrog, Squirrel.