2026-07-22T11:59:29Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18382 2024-03-06T11:01:45Z ddc:004 open_access

A Proof-Producing Compiler for Blockchain Applications Avigad, Jeremy Goldberg, Lior Levit, David Seginer, Yoav Titelman, Alon formal verification smart contracts interactive proof systems Cairo is a programming language for running decentralized applications (dapps) at scale. Programs written in the Cairo language are compiled to machine code for the Cairo CPU architecture, and cryptographic protocols are used to verify the results of the execution traces efficiently on blockchain. We explain how we have extended the Cairo 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 computations with an elliptic curve over a large finite field, as well as their use in the validation of cryptographic signatures. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jeremy Avigad and Lior Goldberg and David Levit and Yoav Seginer and Alon Titelman 2023 Is Part Of LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2023.7 urn:nbn:de:0030-drops-183820 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.7 eng https://creativecommons.org/licenses/by/4.0/legalcode