Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL

Diego Marmsoler

This report presents mechanized query-bounded soundness for a STARK-style protocol in Isabelle/HOL. An acceptance-preserving embedding connects adaptive, privately randomized Fiat-…