n2v Software Tool
n2v: Neural Network Verification in Python
n2v is a Python translation of the MATLAB NNV toolbox by the VeriVITAL research group. It verifies properties of neural networks using sound set-based reachability analysis — star sets and ImageStars among its set representations — and probabilistic verification via conformal inference, which provides coverage guarantees for networks that are intractable to analyse exactly.
n2v supports PyTorch models and ONNX networks, using the model transformation tool onnx2torch to load and convert ONNX models to PyTorch. Its verification methods span exact (sound and complete) star splitting, sound over-approximation, and model-agnostic probabilistic reachability, complemented by counterexample search (falsification) via random sampling and projected gradient descent.