Formalizing Soundness Proofs of Linear PCP SNARKs

Watch a 13-minute conference presentation from USENIX Security '24 exploring the formalization of soundness proofs for linear PCP SNARKs. Learn how researchers from the University of Illinois at Urbana-Champaign developed a formal framework using the Lean theorem prover to validate security properties of Succinct Non-interactive Arguments of Knowledge (SNARKs). Discover their innovative decision procedure for checking SNARK soundness, including its application to notable constructions like Groth '16. Understand the importance of rigorous security proof validation in cryptographic protocols and how this research contributes to identifying and correcting potential flaws in SNARK implementations.