Formalizes a STARK in Isabelle/HOL, with executable prover/verifier models and staged soundness bounds, because math wasn't enough.