Leo: A Programming Language for Formally Verified, Zero-Knowledge Applications

Collin Chin; Howard Wu; Raymond Chu; Alessandro Coglio; Eric McCarthy; Eric Smith

Paper 2021/651

Leo: A Programming Language for Formally Verified, Zero-Knowledge Applications

Collin Chin, Howard Wu, Raymond Chu, Alessandro Coglio, Eric McCarthy, and Eric Smith

Abstract

Decentralized ledgers that support rich applications suffer from three limitations. First, applications are provisioned tiny execution environments with limited running time, minimal stack size, and restrictive instruction sets. Second, applications must reveal their state transition, enabling miner frontrunning attacks and consensus instability. Third, applications offer weak guarantees of correctness and safety. We design, implement, and evaluate Leo, a new programming language designed for formally verified, zero-knowledge applications. Leo provisions a powerful execution environment that is not restricted in running time, stack size, or instruction sets. Besides offering application privacy and mitigating miner-extractable value (MEV), Leo achieves two fundamental properties. First, applications are formally verified with respect to their high-level specification. Second, applications can be succinctly verified by anyone, regardless of the size of application. Leo is the first known programming language to introduce a testing framework, package registry, import resolver, remote compiler, formally defined language, and theorem prover for general-purpose, zero-knowledge applications.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Preprint. MINOR revision.
Keywords: decentralized applications zero-knowledge proofs programming languages formal methods
Contact author(s): howard @ aleo org
History: 2021-05-20: received
Short URL: https://ia.cr/2021/651
License: CC BY

BibTeX

@misc{cryptoeprint:2021/651,
      author = {Collin Chin and Howard Wu and Raymond Chu and Alessandro Coglio and Eric McCarthy and Eric Smith},
      title = {Leo: A Programming Language for Formally Verified, Zero-Knowledge Applications},
      howpublished = {Cryptology ePrint Archive, Paper 2021/651},
      year = {2021},
      note = {\url{https://eprint.iacr.org/2021/651}},
      url = {https://eprint.iacr.org/2021/651}
}