BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Compositional Verification of Cryptographic Proofs in Lean - Quang
  Dao (CMU)
DTSTART:20251007T100000Z
DTEND:20251007T110000Z
UID:TALK237343@talks.cam.ac.uk
CONTACT:Léo Stefanesco
DESCRIPTION:Succinct non-interactive arguments of knowledge (SNARKs) are 
 short\, easily verifiable proofs that an untrusted party executed a comput
 ation correctly. They are nearing wide adoption for applications like priv
 ate identity verification and blockchain scaling\, yet subtle bugs in thei
 r design and implementation remain common\, with severe consequences if e
 xploited.\n\nIn this talk\, I present ongoing work on ArkLib\, an open-sou
 rce Lean library for building SNARKs with machine-checked guarantees of co
 mpleteness and soundness. At the core of ArkLib is a formalization of Int
 eractive Oracle Reductions (IORs)\, a recent abstraction that unifies reas
 oning about common SNARK building blocks. By decomposing complex proof sys
 tems into a series of IORs between simpler relations\, ArkLib enables modu
 lar specifications and security proofs: we can verify components in isolat
 ion and systematically lift their guarantees to full protocols.\n\nI will 
 walk through ArkLib's verification methodology on a representative example
 \, the sum-check protocol\, and close with how AI tools and open collabora
 tion are speeding up the library’s development.\n
LOCATION:LT2\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR