Welcome to the resource topic for 2021/651
Title:
Leo: A Programming Language for Formally Verified, Zero-Knowledge Applications
Authors: Collin Chin, Howard Wu, Raymond Chu, Alessandro Coglio, Eric McCarthy, 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.
ePrint: https://eprint.iacr.org/2021/651
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .