SWIRL is the STARK proof system behind every OpenVM zero-knowledge proof. We prove in Lean that its interactive oracle proof is round-by-round knowledge sound with an exact error bound, building on a verified proximity-gap result.
The SWIRL IOP is composed of several phases comprised of algebraic reductions turning circuit satisfiability constraints into polynomial opening claims checked using WHIR. We analyze the RBR knowledge soundness of SWIRL by composing the security analysis of each phase. The security analysis of WHIR relies on proving bounds concerning the proximity of Reed-Solomon codes.
