Formal verification of the S-two AIR
2026-06-03 • Cryptography and Security
Cryptography and SecurityLogic in Computer ScienceProgramming Languages
AI summaryⓘ
The authors explain how StarkWare's S-two prover helps prove that a program written in the Cairo language runs correctly on a blockchain. They use a special way to describe the program called an algebraic intermediate representation (AIR), which turns the program's behavior into math problems to solve. A cryptographic method called circle STARK gives a proof that these math problems really represent the program running correctly. The authors used a tool called Lean 4 to verify that this translation from program to math is accurate, ensuring the proof is trustworthy.
StarkWareS-two proverCairo languageAlgebraic Intermediate Representation (AIR)Finite fieldcircle STARKCryptographic proofLean 4 proof assistantBlockchainInteractive proof system
Authors
Jeremy Avigad, Anat Ganor, Lior Goldberg, David Levit, Ohad Nir, Yoav Seginer, Alon Titelman
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.