Formal verification of S-two AIR published using Lean 4 proof assistant

StarkWare/S-two

A peer-reviewed paper published formal verification of StarkWare's S-two AIR (Algebraic Intermediate Representation) using the Lean 4 proof assistant, confirming that the AIR encoding is sound and that satisfiability of the AIR implies the computational claim.