A Proof-Producing Compiler for Blockchain Applications

TL;DR

The paper presents a framework to verify CairoZero programs end-to-end by automatically generating Lean proofs that compiled machine code satisfies high-level specifications within a STARK-based blockchain setting. It models the Cairo machine, translates CairoZero code to assembly and then to machine code, and builds autogenerated specifications that users can refine with their own. The authors demonstrate scalable verification on cryptographic primitives (secp256k1 and secp256r1 elliptic curves), digital signature recovery, and a read-only dictionary mechanism, supported by Lean proofs and extensive tooling. This approach enables production-grade verification without obstructing compiler development and paves the way for formally certified Cairo ecosystems, with plans to port insights to the newer Cairo language and Lean 4. The work provides a practical, interactive workflow where automated proof generation is complemented by user-guided specifications, enhancing trust in blockchain-executed dApps.

Abstract

CairoZero is a programming language for running decentralized applications (dApps) at scale. Programs written in the CairoZero language are compiled to machine code for the Cairo CPU architecture and cryptographic protocols are used to verify the results of execution efficiently on blockchain. We explain how we have extended the CairoZero compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications. We demonstrate the success of our approach by verifying primitives for computation with the secp256k1 and secp256r1 curves over a large finite field as well as the validation of cryptographic signatures using the former. We also verify a mechanism for simulating a read-write dictionary data structure in a read-only setting. Finally, we reflect on our methodology and discuss some of the benefits of our approach.