Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL
2026-08-03 • Logic in Computer Science
Logic in Computer ScienceSoftware Engineering
AI summaryⓘ
The authors created a detailed, computer-checked version of a STARK proof protocol using Isabelle/HOL, a tool for formal verification. They built both the prover and verifier as working models, and developed a way to reason about probabilistic behaviors in the system. Their work includes proofs that show the protocol works correctly when honest, and that it is sound up to a known error probability. The focus is mainly on the formal definitions, proof structure, and where to find the key parts in the Isabelle code, aimed at readers familiar with formal methods.
Isabelle/HOLSTARKtransparent proofsproververifierprobabilistic state monadweakest-precondition calculushonest completenesssoundness theoremformal verification
Authors
Diego Marmsoler
Abstract
This report describes an Isabelle/HOL formalization of a STARK-style transparent proof protocol. The development contains an executable model of the prover and verifier, a finite probabilistic state monad with a weakest-precondition calculus, a zero-failure honestcompleteness theorem, and a staged soundness theorem with an explicit probability bound. The report is written for readers with a formal-methods background. It gives enough cryptographic context to explain the protocol, but its main emphasis is the formal model, the decomposition of the proofs, and the Isabelle source locations of the principal definitions and theorems.