LLZK: MLIR-based intermediate representation connecting ZK frontends to verification backends
================================================================================

LLZK is a shared intermediate representation for ZK circuits built on MLIR. Frontends for Circom, Halo2 and Plonky3 (Noir in progress) lower into it, and backends emit Picus queries, zkLean models, R1CS and Rocq via Formal Land's rocq-of-llzk, so one circuit can be checked automatically and then proved.

Maintainer: Veridise (Ethereum Foundation grant)
Website: https://github.com/project-llzk
Category: ZK circuit verification
Targets: Circom, Halo2, Plonky3, Noir (in progress)
Approach: Shared MLIR dialect; lowers to Picus, zkLean, R1CS and Rocq (via Formal Land's rocq-of-llzk)
Access: Open source
Status: Active, v1.0 released 2026-04-08
Strengths: Decouples frontend language from verification backend. | Backed by an EF grant and adopted by Galois and Formal Land backends. | Makes SP1 and RISC Zero style verification repeatable.
Limits: Infrastructure rather than a verifier; you still need a backend and a spec. | Noir frontend incomplete at v1.0. | Adds a translation step to the trusted computing base.
Firms using it: Galois, Veridise, Formal Land
Sources: https://veridise.com/blog/veridise-announcements/llzk-v1-0-a-new-phase-for-zk-shared-infrastructure/ | https://github.com/project-llzk

Source page: https://sorryfree.com/frameworks/llzk/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13