CIVER
Direct answerCIVER is a verifier built into a fork of the Circom compiler by the team behind Circom's own maintainers' academic group. It checks weak safety (every output determined by inputs), tag specifications and user-written pre- and post-conditions template by template, reusing results bottom-up so large circomlib-style codebases scale.
- Maintainer
- COSTA group, Universidad Complutense de Madrid (Albert Rubio et al.)
- Website
- https://github.com/costa-group/circom_civer
- Repository
- https://github.com/costa-group/circom_civer
- Category
- ZK circuit verification
- Targets
- Circom 2.1.6
- Approach
- Z3-backed weak safety (determinism), tag specifications, pre- and post-conditions, verified bottom-up per template
- Access
- Open source (GPL)
- Status (2026-09-13)
- Research, maintained; R1CS, PLONK and ACIR support planned
What CIVER does
Because it runs inside the compiler, CIVER sees the circuit exactly as compiled, avoiding the extraction gap. Its post-condition mode is a lightweight route to functional properties without a proof assistant.
Where it is strong
- No extraction step; verifies what the compiler emits.
- Modular, so circomlib-scale codebases are feasible.
- Supports functional pre- and post-conditions, not just determinism.
Limits and caveats
- Circom only, pinned to a compiler version.
- SMT limits: timeouts on nonlinear-heavy templates.
- Academic maintenance cadence.
When to choose it
Run CIVER alongside Picus on Circom; use its post-conditions to state the properties an audit cares about.
Who works with CIVER
No firm on this index lists CIVER 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, Circomspect, zkFuzz, Coda, Ecne, NAVe, Verified Cairo AIR (Stone and S-two).