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


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.

Available format(s)
Publication info
Preprint. MINOR revision.
decentralized applicationszero-knowledge proofsprogramming languagesformal methods
Contact author(s)
howard @ aleo org
2021-05-20: received
Short URL
Creative Commons Attribution


      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{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.