REVIEW 3 minor 1 cited by
Formal verification of the S-two AIR
T0 review · 0 major / 3 minor · reviewed 2026-06-28 · grok-4.3
Pith's one-line read Satisfiability of the S-two AIR implies that the claimed Cairo program ran to completion.
desk verdict A completed Lean 4 proof that the S-two AIR implies correct Cairo execution. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The Lean 4 formalization of both the AIR algebraic constraints and the operational semantics of the Cairo virtual machine.
What would settle it
An explicit Cairo program together with field-element tables that satisfy every AIR constraint yet produce a final state different from the one required by the Cairo operational semantics.
Extended reading notes
Core claim
The AIR encoding is sound: the existence of satisfying tables for the AIR constraints entails that the corresponding Cairo program reaches the end of its execution trace with the claimed final state.
Load-bearing premise
The Lean 4 definitions match the intended AIR constraints and the actual Cairo virtual-machine execution rules used in S-two.
Editorial extensions
If this is right
- A circle STARK proof that the AIR is satisfied yields a verified certificate that the Cairo program executed correctly.
- Any mismatch between the AIR and the Cairo semantics would allow an incorrect execution trace to produce a valid-looking proof.
- The soundness result applies uniformly to all programs written in the Cairo language that the S-two prover accepts.
Reading between the lines
- The same Lean formalization could be reused to verify AIR soundness for future variants of the Cairo machine or for other STARK-based provers that adopt similar encodings.
- If the AIR constraints were shown to be complete as well as sound, the two directions together would establish equivalence between the AIR and the Cairo execution model.
- Concrete test cases could be extracted from the Lean proof to check that small Cairo programs produce the expected AIR tables.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper describes a Lean 4 formal verification establishing the soundness of the S-two AIR for StarkWare's Cairo virtual machine: satisfiability of the formalized AIR constraints implies that the Cairo program executes to completion according to its operational semantics. The verification is presented as a completed, machine-checked proof against external definitions of the AIR and Cairo semantics.
Significance. If the formalization is faithful, the result supplies machine-checked, parameter-free evidence for the correctness of a production component in a blockchain zero-knowledge proving system. The direct verification against external definitions (rather than reduction to fitted parameters) is a clear strength and addresses the modeling gap that would otherwise remain between the AIR and the VM semantics.
minor comments (3)
- Abstract: the phrase 'the computational claim' is used without a one-sentence gloss of what that claim consists in; a brief inline definition would help readers who are not already familiar with the Cairo execution model.
- The manuscript should include an explicit pointer (URL or repository reference) to the Lean 4 sources so that the formalization can be inspected and re-checked independently.
- A short discussion of the scope of the formalization (e.g., which Cairo opcodes or memory models are covered and which are left as axioms) would clarify the precise boundary of the soundness guarantee.
Simulated Author's Rebuttal
We thank the referee for their positive assessment of the manuscript and for recommending minor revision. We will address any editorial or minor points in the revised version.
Circularity Check
No significant circularity; machine-checked formal proof
full rationale
The paper's central result is a Lean 4 formalization establishing that AIR satisfiability implies the Cairo computational claim. This is a direct, parameter-free, machine-checked proof against external definitions of the AIR constraints and VM operational semantics. No equations reduce to fitted inputs, no self-citations bear the load of the soundness claim, and the verification itself constitutes independent evidence rather than a renaming or self-definition. The modeling step is explicitly the contribution being verified.
Assumptions & free parameters
assumptions (1)
- domain assumption The AIR constraints correctly encode the Cairo VM semantics.
Cite this review
Pith. "Pith review of Formal verification of the S-two AIR." pith.science (2026). https://pith.science/paper/7VELAELS
@misc{pith2026260604311,
author = {Pith},
title = {Pith review of: Formal verification of the S-two AIR},
year = {2026},
howpublished = {\url{https://pith.science/paper/7VELAELS}},
note = {Machine review of arXiv:2606.04311}
}
read the original abstract
StarkWare's S-two prover provides an efficient means for establishing, on blockchain, that a program written in the Cairo virtual machine language runs to completion. The latter claim is encoded by an algebraic intermediate representation (AIR) that captures the semantics of the Cairo language. The AIR asserts the existence of tables of values from a finite field satisfying certain algebraic constraints. A cryptographic interactive proof system, circle STARK, provides an efficiently-checked certificate that the AIR is satisfied. We describe our verification, using the Lean 4 proof assistant, that the AIR encoding is sound, which is to say, the satisfiability of the AIR implies the computational claim.
Forward citations
Cited by 1 Pith paper
-
ZKP Security Tools and Verification: Coverage, Effectiveness, Adoption, and Challenges
Six Circom-focused ZKP tools detect 45.7% of 70 real bugs in isolation but only 19.6% on full codebases; formal verification is mostly constraint-soundness, and practitioners still run human-led workflows with heavy LLM use.
Reference graph
Works this paper leans on
-
[1]
A verified algebraic representation of
Jeremy Avigad and Lior Goldberg and David Levit and Yoav Seginer and Alon Titelman , editor =. A verified algebraic representation of. Certified Programs and Proofs (CPP) 2022 , pages =. 2022 , doi =
2022
-
[2]
Jeremy Avigad and Lior Goldberg and David Levit and Yoav Seginer and Alon Titelman , title =. J. Autom. Reason. , volume =. 2025 , url =. doi:10.1007/S10817-025-09723-Y , timestamp =
-
[3]
Foundations , year =
Jeremy Avigad , booktitle =. Foundations , year =
-
[4]
Leonardo de Moura and Sebastian Ullrich , editor =. The. Conference on Automated Deduction (CADE) 2021 , pages =. 2021 , doi =
2021
-
[5]
2021 , note =
Lior Goldberg and Shahar Papini and Michael Riabzev , title =. 2021 , note =
2021
-
[6]
2022 , url =
Ulrich Hab\"ock , title =. 2022 , url =
2022
-
[7]
2024 , url =
Ulrich Hab\"ock and David Levit and Shahar Papini , title =. 2024 , url =
2024
-
[8]
Interactive Theorem Proving and Program Development -
Yves Bertot and Pierre Cast. Interactive Theorem Proving and Program Development -
Show all 11 references
-
[9]
Paulson and Markus Wenzel , title =
Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel , title =
-
[10]
Certified Programs and Proofs (CPP) 2020 , pages =
The. Certified Programs and Proofs (CPP) 2020 , pages =. 2020 , doi =
2020
-
[11]
Cairo Verification , howpublished =
Reviewed June 28, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.