zkLean

zkLean is a domain specific language (DSL) in Lean for specifying zero-knowledge statements

Development

To compile the zkLean library do:

lake build

The Main.lean file contains some examples of using the library.

A more comprehensive use of the library is done by the companion project for automatic extraction of Jolt circuits into circuits specified with ZkLean (repo available soon, TODO: insert link when zklean-extractor is upstreamed).