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

Abstract

This report presents mechanized query-bounded soundness for a STARK-style protocol in Isabelle/HOL. An acceptance-preserving embedding connects adaptive, privately randomized Fiat-Shamir transcript producers to an established staged adversary experiment and the original probabilistic verifier. The proof combines FRI correlated-agreement reasoning, Merkle authentication, exact modulo-sampler accounting and weighted-path amplification. Event-sensitive accounting refines the complete error bound without changing the verifier or treating repeated oracle calls as free. For a certified 192-bit prime field, trace length 1024 and 640 query repetitions, the concrete theorem bounds false-endpoint acceptance by $2^{-137}$ for every modeled producer satisfying the uniform syntactic oracle-call bound fs_query_bound $(2^{20})$ P. A separate honest-completeness theorem gives acceptance one for the correct square-sequence endpoint in the same final verifier. These are fixed-statement results in a classical, field-valued random-oracle model with terminating finite-support computation, not an unrestricted 137-bit work-factor guarantee. The development does not prove zero knowledge, knowledge extraction, quantum-query security or correctness of a deployed bit-hash implementation. This report retains earlier proof routes as research history; the accompanying current-results overview and checked theorem manifest identify the principal claims and their assumptions.