StarkWare의 S-two prover는 Cairo 가상 머신 (virtual machine) 언어로 작성된 프로그램이 끝까지 실행된다는 것을 블록체인 상에서 입증할 수 있는 효율적인 수단을 제공합니다. 후자의 주장은 Cairo 언어의 의미론 (semantics)을 포착하는 대수적 중간 표현 (algebraic intermediate representation, AIR)에 의해 인코딩됩니다. 이 AIR는 특정 대수적 제약 조건 (algebraic constraints)을 만족하는 유한체 (finite field)로부터의 값 테이블이 존재함을 단언합니다. 암호학적 대화형 증명 시스템 (cryptographic interactive proof system)인 circle STARK는 AIR가 충족된다는 것을 효율적으로 확인할 수 있는 인증서 (certificate)를 제공합니다. 본 논문에서는 Lean 4 증명 보조 도구 (proof assistant)를 사용하여 AIR 인코딩이 건전 (sound)하다는 것을 검증하였으며, 이는 즉 AIR의 충족 가능성 (satisfiability)이 계산적 주장 (computational claim)을 함의함을 의미합니다.