Verified Cairo AIR (Stone and S-two): StarkWare's Lean 4 soundness proofs of the Cairo VM AIR
================================================================================

StarkWare, with Jeremy Avigad and Yoav Seginer, has proved in Lean 4 that satisfying the Cairo VM's AIR (for both the Stone and S-two provers) implies a correct Cairo execution, and in July 2026 used the same methodology to verify the STRK20 privacy pool with more than 230 theorems.

Maintainer: StarkWare with Jeremy Avigad and Yoav Seginer
Website: https://arxiv.org/abs/2606.04311
Category: ZK circuit verification
Targets: Cairo VM AIR, Stone, S-two
Approach: Lean 4 proofs that AIR satisfiability implies a correct Cairo execution; Sierra-to-CASM building blocks
Access: Open source
Status: Active (paper June 2026); in-house at StarkWare, not a service
Strengths: Whole-VM soundness statement for a deployed prover. | Long track record and academic rigour. | Extended to an application (STRK20).
Limits: Cairo specific and in-house. | Not packaged as a reusable framework. | Completeness is not the headline property.
Firms using it: none listed
Sources: https://arxiv.org/abs/2606.04311 | https://starkware.co/blog/strk20-formal-verification/ | https://github.com/NethermindEth/horus-checker

Source page: https://sorryfree.com/frameworks/verified-cairo/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13