CIVER: Modular SMT verification integrated in a Circom fork
===========================================================

CIVER 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
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: Research, maintained; R1CS, PLONK and ACIR support planned
Strengths: 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: Circom only, pinned to a compiler version. | SMT limits: timeouts on nonlinear-heavy templates. | Academic maintenance cadence.
Firms using it: none listed
Sources: https://github.com/costa-group/circom_civer

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