This repository contains a Go library that transpiles zero-knowledge (ZK) circuits from Go to Lean. In particular, it deals with circuits constructed as part of the gnark proof system.
This makes it possible to take existing gnark circuits and export them to Lean for later formal verification.
This library contains the core of the extractor to be used in conjunction with gnark-lean-extractor which is the interface layer with gnark.
For an overview of how to use this library, see the documentation in gnark-lean-extractor. If you are interested in contributing, or are new to Go, please see our contributing guidelines for more information.