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

Diego Marmsoler

REVIEW 3 major objections 3 minor 8 references

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

T0 review · 3 major / 3 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper claims that a STARK-style proof protocol has been formally machine-checked, yielding an executable prover/verifier, honest completeness with zero failure, and a conditional soundness theorem with an explicit acceptance-probabilit

desk verdict A genuine Isabelle/HOL formalization of a STARK-style protocol with a clean completeness proof and a conditional soundness bound that you can't fully check from the manuscript alone. read the letter →

arxiv 2608.01965 v1 pith:64STZIJP submitted 2026-08-03 cs.LO cs.SE

Diego Marmsoler This is my paper

classification cs.LOcs.SE MSC 68Q60

keywords STARKIsabelle/HOLformalverificationprobabilisticstatemonadsoundnesscompletenessFiat-ShamirMerkletree

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out to show that a representative STARK protocol can be modeled precisely enough for a proof assistant to check both its honest execution and its adversarial soundness. It presents an Isabelle/HOL development with an executable prover and verifier, a finite probability monad with a weakest-precondition calculus, a completeness theorem (honest valid traces accepted with probability one), and a staged soundness theorem. The soundness theorem states that when the statement is false and the adversary obeys certain semantic budgets—bounded hash-collision probability, bounded target-hit probability, and hash-map preservation—the verifier accepts with probability at most an explicit sum of collision, query, composition, and FRI error terms. A sympathetic reader cares because this turns a complex cryptographic argument into a mechanically auditable object, and because the explicit bound makes the protocol's security assumptions visible and open to later refinement.

What carries the argument

The workhorse is a finite probabilistic state monad with a weakest-precondition operator (wp_event) for computing probabilities of program events. The protocol is encoded as executable programs in this monad, with a shared channel/transcript/random-oracle state and a Merkle-tree interface. The soundness proof runs a staged experiment where an adversary builds a transcript and then the verifier is re-run with local counters reset; the adversary is constrained by semantic budget predicates. The key evidence object is the authenticated partial opening—root, index, value, path—because that is exactly what the verifier samples, and the proof deliberately avoids assuming sampled openings determine

What would settle it

Inspect the Isabelle sources at the stated commit for a budget record and adversary satisfying the premises where the acceptance probability exceeds the concrete bound—this would refute the theorem. More modestly, try to instantiate the budget record for the GF(5) example with a false statement and check whether the explicit bound is strictly less than 1; if the bound is trivially 1 (or larger) for all reachable parameters, the soundness theorem is formally true but says nothing about practical rejection probability.

Watch

Extended reading notes

Core claim

The central discovery is the decomposition of STARK soundness into a chain of verifier-observed evidence and bounded bad events, phrased over authenticated partial openings rather than reconstructed full tables. The proof shows that any accepting execution of a false statement must fall into at least one of several bad events: hash-output collisions, Fiat-Shamir challenge target hits, query misses, Merkle inconsistencies, or FRI low-degree failures. Each event is bounded separately, and the final public theorem stark_soundness sums them into the concrete bound concrete_restricted_trace_stark_soundness_bound_for. This makes the security argument both explicit and modular: later work can stren

Load-bearing premise

The load-bearing premise is the semantic budget predicate 'staged_adversary_controlled', which assumes the adversary's hash collisions, target hits, and hash-map behavior are bounded; since these bounds are not derived from any concrete hash function, the soundness theorem only covers adversaries that satisfy them.

Editorial extensions

If this is right

If the soundness theorem is correct, instantiating the budget parameters with concrete cryptographic primitives yields a machine-checked conditional security bound for that instantiation.
The probabilistic monad and weakest-precondition calculus are reusable infrastructure for formalizing other probabilistic cryptographic protocols.
The explicit structured bound allows auditors to see which error source dominates and to sharpen collision, query, or FRI terms without changing the public theorem.
The executable square-sequence example over GF(5) demonstrates that the formal model is actual running code, not just an axiomatic description.
The zero-failure completeness theorem gives a formal guarantee that any honest trace satisfying the algebraic validity predicate passes all verifier checks.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Because the adversary budgets are semantic assumptions rather than derived properties of a concrete hash function, the theorem's practical force depends on a future proof that a real hash model satisfies those predicates; otherwise the guarantee is conditional on a possibly empty class of adversaries.
The partial-opening design pattern—work only with evidence the verifier actually sees—looks transferable to the mechanization of other interactive-oracle proofs, where full-table reconstruction is usually too strong.
A natural test of the framework is to instantiate the budget record with a concrete finite-field/hash configuration and see whether the bound remains below 1; if the bound collapses to a tautology in every useful parameter regime, the explicit-bound contribution is mainly architectural.
The separation of public theorems from proof infrastructure is itself a maintainability claim: it suggests that swapping the FRI analysis or the query sampler will not force users of the final theorem to reprove the whole event decomposition.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Diego,

This is a real artifact paper. The Isabelle development implements an executable STARK prover and verifier in a small probabilistic state monad with a weakest-precondition calculus, proves honest completeness with zero failure probability, and states a staged soundness theorem with an explicit bound split into collision, target, query, and FRI terms. If you work on formalized argument systems, this is worth your time.

The genuinely new parts are the proof-engineering choices. The paper deliberately reasons about authenticated partial openings rather than reconstructed full tables, uses prefix-fixed target accounting to keep Fiat-Shamir ordering honest, and separates evidence extraction from residual probability bounds. Section 8 is a useful record of why simpler direct routes fail. The theory layout with stable Isabelle anchors is a model for how artifact papers should be written. I believe the completeness proof is as claimed: the WP reduction to a no-failure support statement is the right structure, and the material in Sections 5.1–5.3 is coherent.

The soft spot is exactly where the stress-test note points. The final soundness theorem is conditional on staged_adversary_controlled, and the concrete bound concrete_restricted_trace_stark_soundness_bound_for is only named, not defined in the text. Appendix C gives a prose gloss of the terms but not the actual definitions. So you cannot tell from the manuscript whether the bound is nontrivial or whether any real adversary can satisfy the budget predicates. The paper is honest about this: Section 10 says instantiations are future work and the bounds are conservative. But as published, the central security claim is unverifiable from the text alone. For a peer-reviewed version, the authors should include the exact predicate and bound definitions, perhaps in a supplementary appendix, and ideally a proof sketch or example that the bound is below 1 for a concrete nonzero budget.

The other limitation is the standard one for this kind of work: the soundness theorem is a conditional framework, not a concrete cryptographic claim. The sampler uniformity and Proth-field assumptions are locale-level premises. The GF(5) example is a sanity check only. None of this detracts from the formalization's value as infrastructure.

My verdict: send it to review. The artifact is substantial, the proof route is novel, and the limitations are stated rather than hidden. The referee should build the repository and check that the named theorems match the prose; if they do, this is a solid contribution to the AFPs and to the literature on verified proof systems. I'd cite it if I were doing STARK formalization.

Referee Report

3 major / 3 minor

Summary. The paper reports on an Isabelle/HOL formalization of a STARK-style transparent proof protocol, with an executable prover/verifier, a finite probabilistic state monad with a weakest-precondition calculus, a zero-failure honest-completeness theorem, and a staged soundness theorem giving an explicit acceptance-probability bound. The presentation is organized around Isabelle theory anchors and describes the proof architecture: transcript replay, Merkle partial openings, Fiat-Shamir target accounting, and query/FRI reductions. The main theorem is stated in Isabelle-like syntax as `stark_soundness`, conditional on `false_statement`, `staged_budget_wellformed`, and `staged_adversary_controlled`, bounding acceptance by `concrete_restricted_trace_stark_soundness_bound_for`. The report does not reproduce the definitions of the budget predicates or the concrete bound, and it explicitly leaves their cryptographic instantiation to future work.

Significance. If the artifact is as described, this is a substantial formal-methods contribution: machine-checked completeness and a conditional soundness proof for a realistic STARK protocol, with executable code and an explicit decomposition of error terms. The report is unusually honest about limitations: the budget interface is semantic, the bounds are conservative, and no concrete hash-function instantiation is proved. The main unmet need is that the statement of the central theorem, as presented in the paper, is not self-contained: the bound and assumptions are named but not defined, so non-vacuity and the claimed explicitness cannot be checked from the manuscript alone.

major comments (3)

[§6.3, Appendix C] The central theorem is not self-contained. `stark_soundness` mentions `concrete_restricted_trace_stark_soundness_bound_for budgets A`, `staged_budget_wellformed`, and `staged_adversary_controlled`, but the manuscript only gives prose descriptions and theory names. The claimed 'explicit probability bound' is thus not stated in the paper. Please include the actual Isabelle definitions (or a faithful human-readable transcription) of the budget record, the well-formedness predicate, the controlled-adversary predicate, and the concrete bound, and give at least one concrete parameter instance with the resulting numeric bound. This is necessary for the reader to assess non-vacuity and whether the bound can be less than 1.
[§6.1, §10, C.1] The soundness theorem is conditional on a semantic adversary interface that, as the paper admits, is not discharged for any concrete hash function. This is a legitimate conditional statement, but the paper should address satisfiability. If no adversary satisfies `staged_adversary_controlled` for a nontrivial budget record, or if the budget fields are chosen so that the bound is trivially at least 1, the result says nothing about actual security. Please exhibit a nontrivial budget record and adversary for which the predicates hold, or state a meta-theorem that the budget interface is satisfiable by every (or a natural class of) staged adversaries.
[§4, §6.3, displayed theorem] The displayed `stark_soundness` theorem lists only three assumptions, yet the text says the core locale fixes exact-order, query-sampler uniformity, Proth-field, and degree well-formedness assumptions. If the theorem is meant to be read inside the soundness locale, that context should be stated in the theorem display; otherwise the statement is under-specified. Please present the fully closed theorem (including locale `fixes`/`assumes`) or explicitly say that the displayed theorem inherits the soundness-locale assumptions.

minor comments (3)

[Title, §1] The title says 'zk-STARK' but the formalization covers completeness and soundness only; no zero-knowledge property is stated or proved. The introduction correctly says 'STARK-style transparent proof protocol', so the title/abstract should be adjusted to avoid overclaiming.
[References] Reference [AF86] lists the authors as 'Adi Shamir Amos Fiat'; this should be 'A. Fiat and A. Shamir'.
[§5] The completeness theorem is displayed as an inequality `≤ 0`. Since probabilities are nonnegative this is equivalent to zero, but the companion equality `completeness_wp_reduction` could be presented as the main theorem to make the zero-failure claim more direct.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the soundness theorem is a conditional machine-checked statement whose bound is derived from protocol events; budget predicates are explicit assumptions, not fitted outputs.

full rationale

The paper's central claims are a zero-failure honest-completeness theorem and a staged soundness theorem with an explicit probability bound, both proved inside Isabelle/HOL against an executable prover/verifier model. The soundness theorem is conditional on the semantic budget predicate `staged_adversary_controlled budgets A` and on the well-formedness of a budget record. This is a standard conditional security statement, not a circular one: the conclusion bounds `checked_staged_adversary_acceptance_probability A` by `concrete_restricted_trace_stark_soundness_bound_for budgets A`, and nothing in the quoted theorem or prose defines that bound in terms of the acceptance probability itself, nor fits any parameter to the claimed output. The budget predicates are explicitly described as semantic upper bounds for hash-collision, target-hit, and oracle-map behavior (Sections 6.1, 6.3, C.1), to be discharged by a future concrete hash instantiation; the manuscript itself flags this as a limitation and future work. That non-vacuity depends on an instantiation is a limitation, not circularity. The only self-citation is the repository reference [Mar26], which identifies the artifact and is not load-bearing in any derivation. No uniqueness theorem is imported from the author's prior work, no ansatz is smuggled via citation, and no known result is renamed as new. The report's reliance on external references [BSBHR18a, BSBHR18b] for the STARK protocol is background context, not the source of the formal proof. Accordingly, no circular step meeting the evidence bar is present, and the appropriate score is 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The central claim rests on the existence and correctness of the external Isabelle repository, plus the locale assumptions listed above. No numbers are fitted to data; the budget record is an assumed semantic input, not a fitted parameter. No new physical or mathematical entities are postulated; the staged adversary and partial openings are modeling constructs, not entities with independent falsifiable handles.

assumptions (5)

domain assumption The staged adversary satisfies the semantic budget predicates staged_adversary_controlled, including bounded hash-collision probability, target-hit bounds, and hash-map preservation.
Section 6.1 and the theorem statement in Section 6: this is a premise of stark_soundness, not derived from a concrete hash function; the paper leaves this to a future cryptographic instantiation.
domain assumption The query sampler's uniformity and divisibility conditions: the field-element-to-nat projection and modulo reduction yield the exact query distribution.
Section 4 explicitly says exact uniformity depends on the enumeration range and a divisibility condition; these are part of the current protocol interface.
domain assumption Proth-field algebraic domain assumptions: the primitive generator has exact power-of-two order, trace and evaluation lengths divide the field group order, and the shifted evaluation coset is disjoint from trace roots.
Sections 2.6 and 4: these are locale assumptions in Core/Stark.thy (exact_order, eval_domain, the shift condition).
domain assumption Constraint-degree well-formedness: declared constraint degrees are sound for all low-degree trace polynomials.
Section 4: a specification-side condition in the core locale, used for the composition-degree argument.
domain assumption Query-margin condition: the query sample space is large enough relative to the degree bound after clearing denominators.
Section 4: needed for a nontrivial query bound; located in the soundness locale rather than the core protocol locale.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL." pith.science (2026). https://pith.science/paper/64STZIJP

@misc{pith2026260801965,
  author       = {Pith},
  title        = {Pith review of: Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/64STZIJP}},
  note         = {Machine review of arXiv:2608.01965}
}

read the original 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.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

8 extracted references

[1]

How to Prove Yourself: Practical Solutions to Identification and Signature Problems , year =

Amos Fiat,Adi Shamir , journal =. How to Prove Yourself: Practical Solutions to Identification and Signature Problems , year =
[2]

, booktitle =

Merkle, Ralph C. , booktitle =. A Digital Signature Based on a Conventional Encryption Function , year =
[3]

Scalable, transparent, and post-quantum secure computational integrity , year =

Eli Ben-Sasson and Iddo Bentov and Yinon Horesh and Michael Riabzev , howpublished =. Scalable, transparent, and post-quantum secure computational integrity , year =
[4]

2018 , address =

Ben-Sasson, Eli and Bentov, Iddo and Horesh, Yinon and Riabzev, Michael , booktitle =. 2018 , address =. doi:10.4230/LIPIcs.ICALP.2018.14 , isbn =

doi:10.4230/lipics.icalp.2018.14 2018
[5]

Paulson and Markus Wenzel , title =

Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel , title =
[6]

Paulson , title =

Tobias Nipkow and Makarius Wenzel and Lawrence C. Paulson , title =. 2025 , howpublished =

2025
[7]

The Archive of Formal Proofs , year =
[8]

Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL , year =

Diego Marmsoler , howpublished =. Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL , year =

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.

[1] [1]

How to Prove Yourself: Practical Solutions to Identification and Signature Problems , year =

Amos Fiat,Adi Shamir , journal =. How to Prove Yourself: Practical Solutions to Identification and Signature Problems , year =

[2] [2]

, booktitle =

Merkle, Ralph C. , booktitle =. A Digital Signature Based on a Conventional Encryption Function , year =

[3] [3]

Scalable, transparent, and post-quantum secure computational integrity , year =

Eli Ben-Sasson and Iddo Bentov and Yinon Horesh and Michael Riabzev , howpublished =. Scalable, transparent, and post-quantum secure computational integrity , year =

[4] [4]

2018 , address =

Ben-Sasson, Eli and Bentov, Iddo and Horesh, Yinon and Riabzev, Michael , booktitle =. 2018 , address =. doi:10.4230/LIPIcs.ICALP.2018.14 , isbn =

doi:10.4230/lipics.icalp.2018.14 2018

[5] [5]

Paulson and Markus Wenzel , title =

Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel , title =

[6] [6]

Paulson , title =

Tobias Nipkow and Makarius Wenzel and Lawrence C. Paulson , title =. 2025 , howpublished =

2025

[7] [7]

The Archive of Formal Proofs , year =

[8] [8]

Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL , year =

Diego Marmsoler , howpublished =. Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL , year =