Leo: A Programming Language for Formally Verified, ZK Applications
summary
Leo claims a language that compiles ZK apps with mechanically checked compiler passes: a Rust compiler (≈65k LOC, 12 contributors) converts source to an ASG, runs passes (including Hindley-Milner style type inference), then synthesizes circuits; each pass is verified with ACL2 proofs and composed for end-to-end correctness. Benchmarks cover a 256-bit Peterson hash, bubble sort, and least squares; the ASG→R1CS step dominates time. Tooling includes Leo Playground and an IDE, targets include BLS12-377 and pluggable back ends. Deterministic execution only.
AI-written summary · about
chapters (29)
- 0:00Introduction
- 2:22Privacy
- 4:34Challenges
- 5:27Goals
- 6:23Compiler Architecture
- 7:49Type Inference
- 10:23Errors
- 14:16Implementation
- 16:51Conclusion
- 18:58Integration of inherently nondeterministic components
- 20:15Scope of Leo
- 24:23Extensions to ZK Interface
- 25:55Procedural Decomposition
- 26:48Specification Scope
- 27:58Formal Verification
- 30:18Theorem Provers
- 31:48Formally Verified
- 32:38Zero Knowledge
- 33:28Formal Semantics
- 34:53Interoperability
- 36:03Function Signature
- 38:43Interface Interoperability
- 39:28Native Context Execution
- 43:23Conclusions
- 44:43Leos IR
- 45:53Leos AST
- 46:33Polymorphic Type Systems
- 47:53Standardizing Leo
- 49:23Telegram Group
related talks
01h 02mLanguage Design meets Verifying Compilers
39mRust, zig and carbon: Hype, hope or hell programming languages?
42mDeveloping the Wolfram Language Compiler
01h 05mAll the Languages Together
29mTowards Formally Verified Just-In-Time Compilation
42mImplementing Languages for Fun and Profit
51mSynthesis and Verification for All
16mTowards formally secure compilation of verified F* programs against unverified ML(…)