Announcing LLZK: A unified, open-source intermediate representation (IR) for zero-knowledge languages | Smart contract audits from Veridise

Announcing LLZK: A unified, open-source intermediate representation (IR) for zero-knowledge languages

We’re excited to announce that LLZK, our open-source intermediate representation (IR) for zero-knowledge circuits, is now officially launched and available to the public.

Developed by Veridise and supported with a grant from the Ethereum Foundation, LLZK aims to unify the fragmented landscape of ZK development by providing a modular, extensible, and verifiable IR layer that bridges the gap between circuit DSLs and proving backends.

Why LLZK?

As zero-knowledge applications proliferate across use cases, from zkVMs and rollups to privacy-preserving identity protocols, developers face a growing challenge: tool fragmentation.

Every DSL (like Circom, Noir, Halo2, Plonky3) comes with its own quirks, and moving between them or auditing their correctness remains painful. LLZK solves this by acting as a common language between circuit frontends and backends.

Think LLVM, but for ZK.

What is LLZK?

LLZK is a modular intermediate representation for zero-knowledge circuits, designed with the following goals in mind:

  • Multi-language compatibility: Compile circuits written in various DSLs to LLZK.
  • Backend flexibility: Translate to a variety of proving systems (R1CS, AIR, Plonkish, etc.).
  • Support for formal verification: Serve as a foundation for tools like Picus to verify security properties.
  • Optimization-friendly: Enable passes such as constraint simplification and dead code elimination.

LLZK is built on top of MLIR, giving it a rich set of compiler tools and well-defined semantics out of the box.

LLZK in action: Succinct SP1 and Picus

We’ve already used LLZK in production.

Recently, we integrated LLZK with Succinct’s SP1 zkVM, which is written in Plonky3. We translated a set of SP1 core operations into LLZK and then used our formal verifier Picus to check for constraint soundness.

Results:

  • 11 SP1 ops verified with no false positives.
  • One under-constrained operation identified—confirmed and fixed by Succinct.
  • LLZK served as a clean bridge between Plonky3 and Picus, demonstrating the power of a shared IR for verification and analysis.

Who should use LLZK?

LLZK is a developer-focused tool for:

  • ZK application builders who want more backend flexibility.
  • Compiler engineers building new ZK languages or DSLs.
  • Security researchers and auditors looking to analyze circuits across DSLs in a unified format.
  • Proving system developers who want standardized input and richer debugging tools.

Explore the tech

LLZK comes with:

  • llzk-lib (C++): A high-performance compiler core built on MLIR.
  • llzk-rs (Rust): A Rust SDK for circuit developers, including bindings, parsers, and utilities.
  • ✅ zirgen-to-llzk: A frontend to compile Zirgen circuits into LLZK.
  • ✅ Sample circuits and integration examples for Zirgen and Succinct’s SP1 circuits (written in Plonky3).
  • ✅ Native support for circuit analysis and R1CS constraint generation.

Documentation, tutorials, and developer onboarding guides are available on GitHub.

Get started:

Teams and projects already building with LLZK

We’re grateful to the Ethereum Foundation’s zkEVM Formal Verification Project for championing the use of LLZK in ZK circuit development.

We’d like to extend warm greetings to Formal Land (building the Rocq proof system), Nethermind (integrating Plonky3), and Galois — excited to see all of you already building on LLZK.

Future plans & ways to connect with LLZK developers

We’re just getting started. As LLZK matures, we plan to add more frontends and backends (including witness generation), deepen integration with Picus and other analysis tools, and enable more real-world projects to adopt LLZK for ZK circuit development and auditing.

We welcome contributions, feedback, and ideas. If you’re interested in working with LLZK, open a PR, file an issue, or reach out to us and write email to Ian or Shankara (their email address is a form of firstname@veridise.com).

Built by Veridise

At Veridise, we specialize in blockchain and ZK security. Our mission is to advance formal methods in blockchain and ZK systems. LLZK is a key part of that vision, bringing principled design, provable correctness, and developer tooling to the ZK world.

We’re proud to open-source LLZK. Our LLZK team, Ian Neal, Tim Hoffman, Daniel Álvarez, and I, can’t wait to see what the community builds with it.

More by Veridise

Subscribe to our blog

Be the first to get the latest from Veridise — including educational articles on ZK and smart contracts, audit case studies, and updates on our tool development. Delivered twice a month.

smart contract audit cloud

Contact us for a security audit quote

Secure an earlier audit slot by reaching out early.