ZkFlow: A Formally Verified Compiler for Zero-Knowledge Circuits

🚧 Under construction 🔐

This post will describe ZkFlow, a small source language and compiler for building zero-knowledge constraint systems, formally verified in Lean.

Will be covered:

• the syntax and semantics of a declarative arithmetic/boolean expression language,
• the ZkLean constraint system DSL developed by Galois for specifying ZK constraints
• how source programs are compiled into circuits
• formal verification of the compiler
• a python script which parses programs in the source language, runs the compiler, and outputs an image of the generated ZK circuit