Getting continuous formal verification into a ZK CI/CD pipeline used to mean one thing: custom integration work, scoped to your language, rebuilt from scratch every time your toolchain evolved. For most ZK teams, that cost was enough to skip it entirely. AuditHub now removes that barrier.
TLDR
- LLZK V1.0 is the first stable shared IR for ZK development.
- Picus and ZK Vanguard now run on any LLZK-targeted language.
- Circom and Halo2 frontends are live; R1CS and zkLean backends ship today.
- Ethereum Foundation funding backs continued development.
What LLZK actually is
LLZK is a shared intermediate representation that sits between ZK front-end languages and backend proving systems. Built on top of MLIR, it models ZK-specific constructs, including constraints and witness generation, using a modular dialect architecture. Language developers compile to LLZK once. From there, any backend or analysis tool built on the IR becomes immediately available.
The MLIR parallel is intentional. Before MLIR, compiler teams rebuilt the same lowering passes for every new front-end. MLIR gave them a common layer to share that work. ZK has been at the same inflection point for years. LLZK is the answer.
What changes for your security workflow
This is where V1.0 has direct practical consequences.
Picus and ZK Vanguard are now LLZK backends. Any language that compiles to the IR can run continuous formal verification of circuit determinism with Picus and static analysis of underconstrained signals, witness leakage, and non-deterministic dataflow with ZK Vanguard, without writing a single line of custom integration code.
For AuditHub, this means CI/CD verification is no longer gated on whether your language had an existing direct integration. Compile to LLZK, and the toolchain follows.
Over 96% of ZK circuit layer bugs stem from underconstrained logic. The language your team builds in should not determine whether those bugs get caught. LLZK removes that dependency.
What shipped in V1.0
Live now: the LLZK repository and documentation, Rust bindings for writing LLZK programs and running compiler passes, Circom and Halo2/PLONKish frontends, and R1CS, zkLean, Picus, and ZK Vanguard backends.
Galois independently built a zkLean backend on LLZK and contributed it without close coordination with the Veridise team. They worked from the public IR, built what they needed, and submitted for review. That is precisely the behavior a shared IR is designed to enable.
LLZK now lives in its own GitHub organization. The Ethereum Foundation funded the initial build and is backing continued development through a second grant.
Coming next: formal specifications in LLZK, enhanced template support for generic structs and functions, and a witness generation backend.
AuditHub coverage expands automatically as LLZK adds new languages
LLZK language developers targeting the IR as their compilation output give their users immediate access to Picus and ZK Vanguard without any additional work. Picus and ZK Vanguard are now native LLZK backends. Any language that compiles to the IR gets direct access to both tools, with no additional integration work required.
RISC Zero integrated Picus into their CI/CD pipeline for continuous verification of their zkVM and detected 35 issues during development. That level of coverage is now accessible without the integration overhead that previously made it impractical.
Ready to run Audithub in your pipeline?
Book a Demo → See how AuditHub connects LLZK formal verification to your existing CI/CD workflow.
Try for Free → Start your free trial and explore Vanguard, OrCa, and Picus today
