Cryptology ePrint Archive: Report 2021/651

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

Collin Chin and Howard Wu and Raymond Chu and Alessandro Coglio and 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.

Category / Keywords: implementation / decentralized applications, zero-knowledge proofs, programming languages, formal methods

Date: received 18 May 2021

Contact author: howard at aleo org

Available format(s): PDF | BibTeX Citation

Version: 20210520:202921 (All versions of this report)

Short URL: ia.cr/2021/651


[ Cryptology ePrint archive ]