A Proof-Producing Compiler for Blockchain Applications
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman

TL;DR
This paper introduces CairoZero, a language and compiler for blockchain applications that includes proof-producing capabilities, enabling formal verification of cryptographic primitives and data structures on the blockchain.
Contribution
We extend the CairoZero compiler with tools for formal verification in Lean 3, allowing high-level specifications to be proved about compiled blockchain code.
Findings
Successfully verified cryptographic primitives for secp256k1 and secp256r1 curves.
Validated cryptographic signatures within the CairoZero framework.
Verified a read-write dictionary mechanism in a read-only setting.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsParallel Computing and Optimization Techniques
