# A verified algebraic representation of Cairo program execution

arXiv: https://arxiv.org/abs/2109.14534 · HTML: https://mlsanity.com/paper/2109.14534/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Sep 2021.

## Built on by (most cited first, 1 of 1)

- [Cryptographic certificates of validity for trustworthy AI](https://mlsanity.com/paper/2606.23768/) (2026)

## Abstract (arXiv)

Cryptographic interactive proof systems provide an efficient and scalable means of verifying the results of computation on blockchain. A prover constructs a proof, off-chain, that the execution of a program on a given input terminates with a certain result. The prover then publishes a certificate that can be verified efficiently and reliably modulo commonly accepted cryptographic assumptions. The method relies on an algebraic encoding of execution traces of programs. Here we report on a verification of the correctness of such an encoding of the Cairo model of computation with respect to the STARK interactive proof system, using the Lean 3 proof assistant.