auto-verify 1.0.0

Efficient portfolio-based verification of neural network properties

Auto-Verify

What is Auto-Verify?

Auto-Verify is a framework that provides an abstraction layer for a range of neural network verifiers, handling their installation, configuration, and execution. The package can be used together with another package by our research group, ada-verona, to simplify the setup of neural network verification experiments for evaluating formal verification tools. For more details, see the How does Auto-Verify work with ada-verona? section in Getting Started.

---

Update November 2025: As of the latest Auto-Verify release v1.0.0, the package also supports L2 Verification via integration of the SDP-CROWN verifier.

See the original SDP-CROWN research repository and the corresponding paper:

SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
ICML 2025
Hong-Ming Chiu, Hao Chen, Huan Zhang, Richard Y. Zhang

---

Installation

We recommend using miniforge to set up the environment for auto-verify.

After Miniconda is installed, setup auto-verify by running the following commands:

conda create -n auto-verify python=3.10
conda activate auto-verify
pip install auto-verify  #or use uv pip if you have uv installed

Getting started

To get started, the How-To Guides offer a useful starting point.

We also recommend having a look at the API documentation.

How do Auto-Verify and ADA-verona relate?

• Auto-Verify wraps neural network verifiers and provides a unified interface for installing, configuring, and running them.
• ADA-verona uses Auto-Verify to easily set up formal verification experiments through its AutoVerifyModule class.

For concrete examples, refer to the examples provided in the ada-verona tutorial.

CLI Commands

You can access the help and examples for the command-line interface by using the --help flag.

auto-verify --help

Installing Verifiers

Currently, auto-verify supports the following verifiers:

• nnenum (Stanley Bak)
• AB-CROWN (Zhang et al.)
• VeriNet (VAS Group)
• Oval-BaB (OVAL Research Group)
• SDP-CROWN (Chiu et al. - OVAL Research Group) – efficient L2-norm robustness verification via semidefinite-program-based bound propagation.

These verifiers can be installed as follows:

auto-verify install nnenum
auto-verify install sdpcrown
auto-verify install abcrown
auto-verify install verinet
auto-verify install ovalbab

You can also install multiple verifiers in one go with the following command:

auto-verify install nnenum abcrown ovalbab verinet sdpcrown

Specifying Verifier Versions

You can specify which version of a verifier to install:

auto-verify install abcrown --verifier-version "877afa32d9d314fcb416436a616e6a5878fdab78"

auto-verify install abcrown --verifier-version most-recent

Note: If a short hash is provided and cannot be resolved, the installation will fall back to the default version for that verifier.

This allows you to:

• Use the default tested stable version
• Install a specific version by commit hash
• Install the latest version from the repository

Environment Selection

You can also specify which environment management strategy to use:

# Force using conda
auto-verify install nnenum --env conda

# Force using venv
auto-verify install nnenum --env venv

Note: We recommend to use the conda option and using miniforge as the package manager.

Listing Installed Verifiers

You can view all installed verifiers with the list command:

# List all installed verifiers
auto-verify list

# List only venv-based verifiers
auto-verify list --env venv

# List only conda-based verifiers
auto-verify list --env conda

# Show detailed information about installed verifiers
auto-verify list --verbose

The verbose mode shows additional information such as:

• Git branch and commit hash
• Path to the virtual environment
• Activation command

Removing Verifiers

To remove installed verifiers:

# Remove a verifier (uninstall command)
auto-verify uninstall nnenum

# Remove multiple verifiers
auto-verify uninstall nnenum abcrown

# Alternative delete command (alias for uninstall)
auto-verify delete nnenum

# Remove only venv-based installations
auto-verify delete nnenum --env venv

# Remove only conda-based installations
auto-verify delete nnenum --env conda

Configuration Options

Auto-verify provides several configuration options to customize its behavior. You can view your current configuration with:

auto-verify config show

Environment Strategy

Controls how verification tool environments are managed:

• conda: Use Conda environments (recommended)
• auto: Automatically detect and use the best available option (prefers venv if uv is available)
• venv: Use Python virtual environments with uv (experimental feature)

# Set environment strategy to venv
auto-verify config set-env venv

# Set environment strategy to conda
auto-verify config set-env conda

# Set environment strategy to auto-detect
auto-verify config set-env auto

Installation Path

Set a custom location for verifier installations:

# Set custom installation path
auto-verify config set-install-path /path/to/custom/location

# Reset to default path
auto-verify config set-install-path default

GPU Preference

Control whether to prefer GPU-enabled installations:

# Enable GPU preference
auto-verify config set-gpu true

# Disable GPU preference
auto-verify config set-gpu false

Default Timeout

Set the default verification timeout (in seconds):

# Set timeout to 300 seconds (5 minutes)
auto-verify config set-timeout 300

Logging Options

Configure logging verbosity:

# Set log level
auto-verify config set-log-level INFO  # Options: DEBUG, INFO, WARNING, ERROR

# Enable verbose installation
auto-verify config set-verbose-installation true

# Disable verbose installation
auto-verify config set-verbose-installation false

Advanced Options

Configure advanced behavior:

# Allow conda fallback if venv+uv is not available
auto-verify config set-conda-fallback true

# Disable conda fallback
auto-verify config set-conda-fallback false

# Require uv when using venv strategy
auto-verify config set-require-uv true

# Make uv optional
auto-verify config set-require-uv false

Other Configuration Commands

# Create example configuration file
auto-verify config example

# Reset all configuration to defaults
auto-verify config reset

Configuration File

You can also edit the configuration file directly:

# Create example configuration file if it doesn't exist
auto-verify config example

# Edit the configuration file with your preferred editor
nano ~/.config/autoverify/autoverify.toml

Available configuration options:

Option	Description	Default	CLI Command
env_strategy	Environment management strategy ("conda", "venv", or "auto")	"auto"	set-env
custom_install_path	Custom location for verifier installations	None (uses XDG data directories)	set-install-path
prefer_gpu	Whether to prefer GPU-enabled installations	true	set-gpu
default_timeout	Default verification timeout in seconds	600	set-timeout
log_level	Logging verbosity ("DEBUG", "INFO", "WARNING", "ERROR")	"INFO"	set-log-level
verbose_installation	Show detailed output during installation	false	set-verbose-installation
allow_conda_fallback	Allow falling back to conda if venv+uv is not available	true	set-conda-fallback
require_uv	Require uv to be installed when using venv strategy	false	set-require-uv

Example configuration file:

# Environment management strategy: "conda", "venv", or "auto"
env_strategy = "venv"

# Custom installation path (optional)
# custom_install_path = "/path/to/custom/location"

# Runtime preferences
prefer_gpu = true
default_timeout = 600

# Logging
log_level = "INFO"
verbose_installation = false

# Advanced options
allow_conda_fallback = true
require_uv = false

Installation Paths

By default, auto-verify uses the following installation paths:

Default Installation Paths

When using the venv strategy, verifiers are installed at:

~/.local/share/autoverify-venv/verifiers/

When using the conda strategy, verifiers are installed at:

~/.local/share/autoverify/verifiers/

Each verifier is installed in its own subdirectory:

# For venv-based installations
~/.local/share/autoverify-venv/verifiers/
├── nnenum/
│   ├── venv/          # Python virtual environment
│   ├── tool/          # Git repository
│   └── activate.sh    # Activation script
├── abcrown/
└── verinet/

# For conda-based installations
~/.local/share/autoverify/verifiers/
├── nnenum/
│   └── tool/          # Git repository
├── abcrown/
└── verinet/

Custom Installation Path

You can set a custom installation path using the CLI or by editing the configuration file:

# Set custom path via CLI
auto-verify config set-install-path /path/to/custom/location

# Set custom path in config file
custom_install_path = "/path/to/custom/location"

When a custom path is set, both venv and conda verifiers will be installed under this directory, maintaining the same structure:

/path/to/custom/location/
├── verifiers/
│   ├── nnenum/
│   ├── abcrown/
│   └── verinet/

Using with ada-verona

Auto-verify can be used as a plugin for the robustness experiment setup package ada-verona, providing formal verification capabilities.