Compositional Formal Verification of SNARKs with ArkLib
No ratings
Presented at Real World Crypto 2026 by
Succinct non-interactive arguments of knowledge (SNARKs) are short, efficiently verifiable proofs that an untrusted party executed a computation correctly. Among many possible use cases, SNARKs have seen adoption as a scaling technology for blockchains, and currently secure billions of dollars in the Ethereum ecosystem. However, deploying SNARKs in production is difficult: the academic literature is rapidly evolving, and addressing performance requirements demands significant engineering efforts. This results in complex, constantly evolving software. Mistakes in either the specification or implementation of a SNARK can and do result in devastating soundness bugs. We present ArkLib, a library in the Lean proof assistant for formally verifying SNARK protocols. ArkLib aims to bridge the gap between cryptographic literature and production code by presenting a unified framework for specifying and mechanically proving the security of SNARKs. The framework's core is a formalization of (functional) Interactive Oracle Reductions (IORs). This abstraction allows us to model protocols like sum-check and FRI as a series of IORs, and prove their security compositionally relying on generic transformations of IORs. To realize this vision, we have developed foundational sub-libraries for oracle computations, computable polynomials, coding theory, and binary tower fields. Our large-scale, open-source effort is aided by AI-assisted formalization; we use AI tools to complete a number of proofs and identify misformalization issues, helping to manage the complexity of the library. While full end-to-end security proofs are ongoing, our work establishes the first mechanized theory of IORs and provides a path toward building verifiably secure SNARKs.