# ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks

arXiv: https://arxiv.org/abs/2407.01639 · HTML: https://mlsanity.com/paper/2407.01639/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 53 references that are in the map.
- First posted on arXiv 30 Jun 2024.

## Builds on (most cited first, 30 of 30)

- [Deep Residual Learning for Image Recognition](https://mlsanity.com/paper/1512.03385/) (2015)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [DeepDriving: Learning Affordance for Direct Perception in Autonomous Driving](https://mlsanity.com/paper/1505.00256/) (2015)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Measuring Neural Net Robustness with Constraints](https://mlsanity.com/paper/1605.07262/) (2016)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results](https://mlsanity.com/paper/2212.10376/) (2022)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Safe Control Under Input Limits with Neural Control Barrier Functions](https://mlsanity.com/paper/2211.11056/) (2022)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations](https://mlsanity.com/paper/1712.08163/) (2017)
- [Safe Control with Neural Network Dynamic Models](https://mlsanity.com/paper/2110.01110/) (2021)
- [Neural Network Repair with Reachability Analysis](https://mlsanity.com/paper/2108.04214/) (2021)
- [The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks](https://mlsanity.com/paper/2301.07068/) (2023)
- [Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees](https://mlsanity.com/paper/2308.09842/) (2023)
- [Safe Control Algorithms Using Energy Functions: A Unified Framework, Benchmark, and New Directions](https://mlsanity.com/paper/1908.01883/) (2019)
- [Towards Hierarchical Task Decomposition using Deep Reinforcement Learning for Pick and Place Subtasks](https://mlsanity.com/paper/2102.04022/) (2021)
- [Reachability Analysis of a General Class of Neural Ordinary Differential Equations](https://mlsanity.com/paper/2207.06531/) (2022)
- [Reachability Analysis and Safety Verification for Neural Network Control Systems](https://mlsanity.com/paper/1805.09944/) (2018)
- [Curriculum Learning for Safe Mapless Navigation](https://mlsanity.com/paper/2112.12490/) (2021)
- [From Design Draft to Real Attire: Unaligned Fashion Image Translation](https://mlsanity.com/paper/2008.01023/) (2020)
- [Meta-Control: Automatic Model-based Control Synthesis for Heterogeneous Robot Skills](https://mlsanity.com/paper/2405.11380/) (2024)

## Built on by (most cited first, 7 of 7)

- [Probabilistically Tightened Linear Relaxation-based Perturbation Analysis for Neural Network Verification](https://mlsanity.com/paper/2507.05405/) (2025)
- [Formal Verification of Variational Quantum Circuits](https://mlsanity.com/paper/2507.10635/) (2025)
- [Provably Safe, Yet Scalable Reinforcement Learning](https://mlsanity.com/paper/2606.14536/) (2026)
- [Enhancing Certifiable Semantic Robustness via Robust Pruning of Deep Neural Networks](https://mlsanity.com/paper/2510.00083/) (2025)
- [From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications](https://mlsanity.com/paper/2603.05604/) (2026)
- [Probabilistic Verification of Recurrent Neural Networks for Single and Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2605.14758/) (2026)
- [A Survey on the Verification of Reinforcement Learning Policies](https://mlsanity.com/paper/2607.16210/) (2026)

## Abstract (arXiv)

Deep Neural Networks (DNN) are crucial in approximating nonlinear functions across diverse applications, ranging from image classification to control. Verifying specific input-output properties can be a highly challenging task due to the lack of a single, self-contained framework that allows a complete range of verification types. To this end, we present textttModelVerification.jl (MV), the first comprehensive, cutting-edge toolbox that contains a suite of state-of-the-art methods for verifying different types of DNNs and safety specifications. This versatile toolbox is designed to empower developers and machine learning practitioners with robust tools for verifying and ensuring the trustworthiness of their DNN models.