Formal verification of the S-two AIR
This paper formally verifies that the algebraic intermediate representation (AIR) used by the S-two prover correctly captures the computational semantics of the Cairo virtual machine language, ensuring that satisfying the AIR implies the program runs to completion.
Abstract
More Like ThisStarkWare'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.