01▲Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL arxiv.org Formalizes a STARK in Isabelle/HOL, with executable prover/verifier models and staged soundness bounds, because math wasn't enough.completenessformal-verificationholisabelleprobabilistic-proofssoundnessstarktwitterzk0 pts/ovoss/9 days ago/discuss