Abstract

Succinct non-interactive arguments of knowledge (SNARKs) are short, easily verifiable proofs that an untrusted party executed a computation correctly. They are nearing wide adoption for applications like private identity verification and blockchain scaling, yet subtle bugs in their design and implementation remain common, with severe consequences if exploited.

In this talk, I present ongoing work on ArkLib, an open-source Lean library for building SNAR Ks with machine-checked guarantees of completeness and soundness. At the core of ArkLib is a formalization of Interactive Oracle Reductions (IORs), a recent abstraction that unifies reasoning about common SNARK building blocks. By decomposing complex proof systems into a series of IORs between simpler relations, ArkLib enables modular specifications and security proofs: we can verify components in isolation and systematically lift their guarantees to full protocols.

I will walk through ArkLib’s verification methodology on a representative example, the sum-check protocol, and close with how AI tools and open collaboration are speeding up the library’s development.