ArkLib: Formally Verified Arguments of Knowledge in Lean

Contributed by Derek Sorensen, Ethereum Foundation

Succinct, non-interactive arguments of knowledge (SNARKs) are cryptographic proof systems that allow one party (the prover) to convince a verifier that a public statement is true with a succinct proof. Proofs are typically far smaller than the computation they attest to, and verification is much cheaper than re-running the work. They underpin a growing range of applications, including privacy-preserving payments, private credential checks, verifiable selective disclosure, and machine-learning inference. They are also central to Ethereum's scaling roadmap: future nodes will use SNARKs to validate blocks by checking a proof rather than re-executing every transaction.

SNARKs are an ideal use-case for formal verification. They are notoriously subtle and difficult to implement with high assurance. Their security proofs are long, probabilistic, and intricate. Depending on the use case, a soundness bug, one that lets a prover convince a verifier of something false, can be catastrophic because an attacker can forge a proof of invalid data or state. ArkLib and a growing ecosystem of associated libraries are infrastructure in Lean to formally verify the security of these cryptographic protocols.

Arguments of Knowledge, Mechanized in Lean🔗

ArkLib is the center of a growing ecosystem of libraries in Lean that target SNARK verification and development at multiple levels.

  • ArkLib: Formally verified arguments of knowledge in Lean, the core library for SNARKs. Formalizes interactive oracle reduction (IOR), sum-check, polynomial commitments, FRI/STIR/WHIR, Fiat–Shamir, and BCS transforms.

  • VCV-io: An oracle framework in Lean for game-based cryptographic proofs, and an essential dependency of ArkLib. ArkLib uses it to model probabilistic adversaries and oracle queries, and to carry out the game-hopping arguments that SNARK security proofs rely on.

  • CompPoly: Computable polynomials and finite fields, ArkLib's executable core and a computable mirror to many of the definitions and functions in Mathlib. Everything in CompPoly is computable, but proofs can still be done using the corresponding Mathlib definitions by transfer over proven equivalences.

  • Clean: a ZK circuit DSL in Lean. Can be used for building high-assurance ZK circuits directly in Lean as well as a ZK circuit specification framework.

  • See the Verified-zkEVM org for iris-lean, evm-asm, and more.

SNARKs in the Wild🔗

Many production provers are implemented in Rust, not Lean. Rust-to-Lean tools like Aeneas or Hax make it possible to extract production Rust code into Lean, where it can be formally verified with respect to ArkLib specifications.

Who Benefits🔗

  • zk and protocol engineers get precise, machine-checked specifications of the protocols they build on, plus executable references to test their implementations against.

  • Cryptography researchers gain a reusable, growing corpus of mechanized proofs — sum-check, FRI, WHIR, and more — to build on rather than reprove.

  • The Lean and Mathlib communities gain a substantial real-world application of formalized mathematics, and the library improvements that flow back from it.

  • Anyone building SNARKs in Lean can use these specifications to formally verify their proof systems; the more people using these libraries, the more mature, generally applicable, and reliable they will become.

Learn More🔗

  • ArkLib — formally verified arguments of knowledge in Lean

  • VCV-io — oracle framework for game-based cryptographic proofs

  • CompPoly — computable polynomials, ArkLib's executable core

  • Clean — zk circuit DSL in Lean

  • Verified zkEVM — the umbrella Ethereum Foundation initiative

  • ethproofs.org — tracking real-time block proving with zkVMs

  • Aeneas — Rust-to-Lean verification (one option for the implementation bridge)

  • Hax — Rust-to-Lean extraction for verification

  • Mathlib — Lean's mathematical library