Lurk is an in-development, Turing-complete programming language for recursive zk-SNARKs.
DISCLAIMER: Lurk is an early research-stage language. Neither the cryptography nor the software has been audited, and there is currently no trusted setup for Groth16 circuits. Do not use Lurk in production environments or anywhere else that security is necessary.
lurk-rs is the Rust implementation of Lurk, which generates binaries via rustc. The Rust implementation supports expression evaluation, proof of correct evaluation, and proof verification. lurk-rs also provides preliminary support for WASM.
lurk is a Common Lisp reference implementation of Lurk. This implementation only supports expression evaluation. The language specification lives in this repo, and the implementation provided there aims for simplicity and demonstration of the intended semantics without the proving tools of lurk-rs.
- Lurk program execution can be proved in zero knowledge.
- Lurk proofs support multiple backend SNARK proving systems.
- Lurk enables incremental computation and proofs in unbounded loops.
- Lurk provides conditional control flow.
- Lurk programs are data and vice versa.
- Lurk data is content-addressable for compatibility with IPLD/IPFS.
Yatima is a dependently typed, content addressed compiler from the Lean Theorem Prover to Lurk. This enables formally verified zk-proofs of execution, whether it's abstract cryptography via FFaCiL.lean or interpreted WebAssembly code via Wasm.lean.
Visit us on the web at https://lurk-lab.com or https://lurk-lang.org.
Come hang out on our Zulip.
Follow @LurkLab on Twitter.
MIT or Apache 2.0
