NNV: Neural Network Verification Toolbox¶
NNV is a MATLAB toolbox for neural network verification using sound set-based reachability analysis. It supports feedforward, convolutional, recurrent, graph, and semantic segmentation networks, as well as neural ODEs and neural network control systems.
Developed by the VeriVITAL research group at Vanderbilt University.
Exact and approximate reachability analysis with Star sets, zonotopes, and abstract domains – formal safety guarantees.
FFNNs, CNNs, RNNs, SSNNs, Neural ODEs, GNNs, Vision Transformers, BNNs, and Neural Network Control Systems.
Conv1D/2D/3D, ReLU, Sigmoid, Tanh, LSTM, GCN, GINE, BatchNorm, MaxPool, and many more – with exact and approximate methods.
Load ONNX models, parse VNNLIB specifications, and run VNN-COMP benchmarks out of the box.
Verify closed-loop systems with NN controllers – linear, nonlinear, discrete, and hybrid automaton plant models via CORA integration.
Proven across 11 competition entries in VNN-COMP and ARCH-COMP, plus 30+ peer-reviewed publications.
Quick Example¶
% Load a neural network from ONNX
dlnet = importNetworkFromONNX('model.onnx', InputDataFormats='BC');
net = matlab2nnv(dlnet);
% Define input set as a Star (L-inf ball around a point)
lb = [0.4; 0.4; 0.4]; % lower bounds
ub = [0.6; 0.6; 0.6]; % upper bounds
input_set = Star(lb, ub);
% Compute reachable output set
reachOptions = struct;
reachOptions.reachMethod = 'approx-star';
output_sets = net.reach(input_set, reachOptions);
% Check safety property: output(1) >= 0
unsafe_region = HalfSpace([1 0], 0); % y1 <= 0
result = verify_specification(output_sets, unsafe_region);
% result: 1 = safe, 0 = unsafe, 2 = unknown
Getting Started¶
Install NNV and run your first neural network verification in minutes.
Set up NNV with MATLAB toolboxes, CORA, and optional Python dependencies for conformal prediction.
Create your first input set, run reachability analysis, and check safety properties.
User Guide¶
Comprehensive guides for all NNV features, from set representations to control system verification.
All supported network types, 48 layer types, the NN and GNN classes, and model loading utilities.
Star, ImageStar, VolumeStar, GraphStar, Zono, Box, and more – mathematical definitions, constructors, and usage guidance.
Exact, approximate, probabilistic, and abstract domain methods – reachOptions, falsification, and result interpretation.
Linear, nonlinear, discrete, and hybrid plant models with neural network controllers and CORA integration.
Load ONNX models, parse VNNLIB specs, and convert between MATLAB and NNV network formats.
linprog, GLPK, and Gurobi – solver comparison, selection, and performance configuration.
Python setup, surrogate model training, and probabilistic verification with coverage guarantees.
Aerospace, automotive, medical imaging, power systems, cybersecurity, fairness, and more.
Run NNV in a Docker container with MATLAB.
API Reference & Developer Guide¶
Function-level documentation and guides for extending NNV.
Architecture overview, custom verification workflows, adding new layers, set types, and reachability methods.
NN, GNN, Star, ImageStar, all 48 layers, NNCS classes, utilities, and reachOptions – complete function signatures.
NNV 3.0¶
See what’s new in NNV 3.0 – VolumeStar, FairNNV, probabilistic verification, weight perturbation analysis, and more.
Examples & Tutorials¶
Worked examples demonstrating NNV’s verification capabilities across 10+ application domains.
MNIST, GTSRB, MedMNIST, CIFAR-10 – adversarial robustness verification for image classifiers.
Aviation collision avoidance – verifying all 45 ACAS Xu networks with ONNX and VNNLIB.
ACC, AEBS, Inverted Pendulum, DC-DC Buck – closed-loop safety verification with NN controllers.
GCN and GINE on IEEE bus systems – verifying neural power flow predictions.
Semantic segmentation, Neural ODEs, RNNs, malware detection, medical imaging, and conference tutorials.
Theoretical Foundations¶
Mathematical details behind NNV’s verification algorithms, set representations, and probabilistic guarantees.
Star set definitions, exact and approximate reachability algorithms, and ReLU splitting strategies.
Extending Star sets to 2D images, 3D volumes, and video data.
Conformal inference, surrogate models, and the coverage-confidence guarantee framework.
Counterfactual fairness, individual fairness, and the Verified Fairness score.
References¶
The methods implemented in NNV are based upon or used in the following publications:
Key Publications
D. Manzanas Lopez, S.W. Choi, H.-D. Tran, T.T. Johnson, “NNV 2.0: The Neural Network Verification Tool,” in Computer Aided Verification (CAV), Springer, 2023. DOI: 10.1007/978-3-031-37703-7_19
H.-D. Tran et al., “NNV: A Tool for Verification of Deep Neural Networks and Learning-Enabled Autonomous Cyber-Physical Systems,” in Computer Aided Verification (CAV), 2020. DOI: 10.1007/978-3-030-53288-8_1
H.-D. Tran, S. Bak, W. Xiang, T.T. Johnson, “Towards Verification of Large Convolutional Neural Networks Using ImageStars,” in Computer Aided Verification (CAV), 2020.
See the full publications list and how to cite.
Acknowledgements¶
This work is supported in part by AFOSR, DARPA, NSF.