Formal verification of the S-two AIR
This work provides a foundational guarantee for the correctness of zero-knowledge proofs on blockchain, addressing the need for trust in cryptographic provers.
The authors formally verified the soundness of the algebraic intermediate representation (AIR) used in StarkWare's S-two prover, proving that satisfiability of the AIR implies the correctness of the computational claim for Cairo programs. The verification was carried out using the Lean 4 proof assistant.
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.