NNV: A Formal Verification Toolbox for Deep Learning Systems

This article introduces NNV, an open-source MATLAB neural network verification tool developed by the VeriVITAL team at Vanderbilt University. It supports formal verification and reachability analysis for various architectures such as feedforward networks, CNNs, RNNs, and GNNs, providing a unified verification framework and multiple set representation methods. The latest version 3.0 adds modules like fairness verification and probabilistic verification to help ensure the safety of AI systems.

Original Authors/Maintainers: VeriVITAL Research Group (Vanderbilt University) Source Platform: GitHub Original Link: https://github.com/verivital/nnv Official Documentation: https://www.verivital.com Release Time: Continuously updated

NNV (Neural Network Verification) is an open-source MATLAB toolbox for formal verification of deep neural networks and learning-based cyber-physical systems. It implements set-based reachability analysis methods, supports multiple set representations like Star sets, and can verify feedforward, convolutional, recurrent, graph neural networks, as well as neural ODEs and neural network control systems.

Supported Architecture Types

• Feedforward Neural Networks (FFNN): Verification of standard fully connected layers
• Convolutional Neural Networks (CNN): ImageStar optimization for high-dimensional image input processing
• Recurrent Neural Networks (RNN/LSTM): Verification of time-series data
• Graph Neural Networks (GNN): GraphStar support for graph-structured data
• Segmentation Networks: Verification for semantic segmentation tasks
• Neural ODEs: Verification of continuous-time neural networks

Reachability Analysis Methods

• Star sets: General convex polyhedron representation, supporting affine transformations and intersection operations
• ImageStars: Star set representation optimized for image data
• VolumeStars: Extended representation considering volume information
• GraphStars: Set representation for GNNs

Users can choose the appropriate set representation based on the scenario to balance efficiency and accuracy.

The latest NNV version 3.0 (tool paper at ATVA2026) adds the following features:

• FairNNV: Fairness verification module to detect decision biases (e.g., scenarios related to sensitive attributes)
• ProbVer: Probabilistic verification framework supporting neural networks with randomness (e.g., Bayesian networks, dropout components)
• GNNV: Graph neural network verification module extending non-Euclidean data processing capabilities
• VideoStar: Support for video data verification, extending ImageStar to the time dimension
• ModelStar: Model-level verification abstraction supporting complex system-level tasks

These features expand the application scope and capabilities of NNV.

Docker Deployment (Recommended)

Two license modes are available:

• Online license mode: Suitable for individual users, activate via browser login
• Network license mode: Suitable for institutional users, unattended batch operation

The Docker image pre-installs MATLAB R2025b and AIVL, supporting GPU acceleration (via the --gpus all parameter).

Reproducibility Experiments

It includes 6 experiments (FairNNV, ProbVer, GNNV, VideoStar, ModelStar, ToolComparison), with smoke test (about 30 minutes) and full run (5-7 hours) modes, which can generate key tables for papers.

Formal verification of neural networks provides mathematical safety guarantees, which is crucial for safety-critical fields such as autonomous driving and aerospace. As a representative open-source tool, NNV has been cited in many academic papers and has an active community.

NNV 3.0 has been comprehensively compared with the MathWorks AI Verification Library (AIVL) in terms of verification time, memory usage, accuracy, etc. The Docker image automatically installs AIVL dependencies, allowing users to compare performance in the same environment. NNV can still run fully even without AIVL.

For users of NNV, the following recommendations are provided:

1. Prioritize Docker environment: Avoid complex MATLAB installation and dependency configuration
2. Run smoke tests: Quickly verify environment correctness
3. Read example code: The project provides rich examples covering different architectures and scenarios
4. Understand set representations: Choosing the right representation affects verification efficiency
5. Follow community updates: The field is developing rapidly, and new methods are continuously integrated

NNV is a cutting-edge tool in the field of neural network verification, and its open-source nature and active maintenance make it an important resource for academia and industry.