Compositional Verification of Cryptographic Proofs in Lean

Add to your list(s) Download to your calendar using vCal

• Quang Dao (CMU)
• Tuesday 07 October 2025, 11:00-12:00
• LT2, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Léo Stefanesco.

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.

This talk is part of the lads2's list series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Computer Architecture Group Meeting
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• LT2, Computer Laboratory, William Gates Building
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk449

Note that ex-directory lists are not shown.