NAVe: Automatic proper-constrainedness checking for Noir
========================================================

NAVe 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: Noir, ACIR
Approach: cvc5 with finite-field SMT-LIB theories
Access: Research
Status: Research (January 2026)
Strengths: Automatic, no spec required. | Targets Noir directly.
Limits: Young research tool. | Solver limits on large programs. | Determinism, not correctness.
Firms using it: none listed
Sources: https://arxiv.org/abs/2601.09372

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