NAVe
Direct answerNAVe checks Noir programs for proper constrainedness using cvc5's finite-field theory, giving the Noir ecosystem an automatic underconstraint detector comparable to Picus for Circom.
- Maintainer
- Pedro Antonino, Namrata Jain
- Website
- https://arxiv.org/abs/2601.09372
- Category
- ZK circuit verification
- Targets
- NoirACIR
- Approach
- cvc5 with finite-field SMT-LIB theories
- Access
- Research
- Status (2026-09-13)
- Research (January 2026)
What NAVe does
Noir compiles to ACIR, which NAVe analyses directly. It is the automatic complement to Lampe's proof-assistant route.
Where it is strong
- Automatic, no spec required.
- Targets Noir directly.
Limits and caveats
- Young research tool.
- Solver limits on large programs.
- Determinism, not correctness.
When to choose it
Run it on Noir circuits as the first pass, then Lampe for proofs.
Who works with NAVe
No firm on this index lists NAVe as a core tool yet; the firms below cover the same problem class.
Top-listed for circuit verification work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Related frameworks in ZK circuit verification
Clean, sp1-lean, zkLean, Halva, Picus, LLZK, Garden, Lampe, proven-zk and gnark-lean-extractor, CIVER, Circomspect, zkFuzz, Coda, Ecne, Verified Cairo AIR (Stone and S-two).