Show HN: Neural Network Formal Verification

A curated list of awesome tools, benchmarks, papers, and resources for the formal verification of neural networks. Formal neural network verification is a set of techniques used to mathematically prove that a neural network satisfies specific properties, such as safety, robustness, or fairness, under all possible inputs within a given range. This is critical for deploying deep learning models in safety-critical domains like autonomous driving, aerospace, robotics, and medicine, where empirical testing is insufficient to guarantee correctness. Contents Exact and complete solvers Abstract interpretation and reachability Branch-and-bound and accelerated verifiers Closed-loop and cyber-physical systems Benchmarks and competitions Literature Surveys Seminal papers Community Exact and complete solvers Marabou - An SMT-based framework for verifying deep neural networks, supporting properties specified via the VNN-LIB format. MIPVerify.jl - A Julia-based verification tool that formulates the neural network robustness certification problem as a mixed-integer linear programming (MILP) optimization problem. Reluplex - A foundational SMT-based solver algorithm designed to verify neural networks with ReLU activations by extending the Simplex method (predecessor to Marabou). Venus - A sound and complete MILP-based verification toolkit utilizing symbolic interval propagation and input domain splitting. Abstract interpretation and reachability auto_LiRPA - A library for automatic linear relaxation-based perturbation analysis (LiRPA) on general computational graphs, serving as a core bound-propagation backend. ERAN - The ETH Robustness Analyzer for Neural Networks, leveraging abstract interpretation with custom domains (such as DeepPoly and RefineZ) to certify neural network safety. Neurify - A symbolic interval analysis verifier with directed constraint refinement for efficient tight bounds. NNV - A MATLAB toolbox performing set-based reachability analysis (using Star sets, ImageStars, and zonotopes) for feedforward, convolutional, and recurrent architectures. pyNeVer - A library for the design, training, and formal verification of neural networks using star-set-based reachability analysis algorithms. Branch-and-bound and accelerated verifiers alpha-beta-CROWN - A GPU-accelerated neural network verifier combining efficient linear bound propagation with branch-and-bound search. MN-BaB - A GPU-based branch-and-bound verifier employing multi-neuron relaxation constraints within DeepPoly abstract domains. nnenum - A high-performance verification tool utilizing multiple abstraction levels including zonotopes, star sets, and LP relaxation. VeriNet - A complete branch-and-bound verification toolkit based on symbolic interval propagation and external LP/MIP optimization. Closed-loop and cyber-physical systems POLAR - A tool for reachability analysis of neural-network-controlled continuous and hybrid systems using Taylor model flowpipes. Verisig - A tool for the formal verification of closed-loop systems with neural network controllers using hybrid automata reachability. Benchmarks and competitions VNN-COMP - The official repository for the international Verification of Neural Networks Competition, hosting standardized benchmarks (in VNN-LIB and ONNX formats) and performance results. Literature Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective (IEEE TDSC, 2022) - A security-centric review of verification methods designed to prove network robustness against adversarial attacks. Algorithms for Verifying Deep Neural Networks (Liu et al., 2019) - A comprehensive survey that provides a unified mathematical framework for neural network verification. Introduction to Neural Network Verification (A. Albarghouthi, 2021) - A foundational textbook-style survey covering key mathematical models, abstractions, and algorithms. Seminal papers AI2: Safety Verification of Deep Neural Networks with Abstract Interpretation (Gehr et al., IEEE S&P 2018) - Pioneered the application of abstract interpretation to deep feedforward and convolutional neural networks. An Abstraction-Refinement Approach to Verification of Artificial Neural Networks (Pulina and Tacchella, CAV 2010) - Formulated early SMT-based verification of neural networks using a counter-example guided abstraction refinement loop. An MIP-Based Approach for Evaluating the Robustness of Deep Neural Networks (Tjeng et al., ICLR 2019) - Showed how mixed-integer programming (MIP) can perform exact robustness verification. Certified Adversarial Robustness via Randomized Smoothing (Cohen et al., ICML 2019) - Established scalable certified robustness guarantees against adversarial perturbations using randomized smoothing. DeepPoly: An Abstract Domain for Proving Safety of Deep Neural Networks (Singh et al., POPL 2019) - Introduced the DeepPoly abstract domain for scalable and precise abstract interpretation of neural networks. Intriguing Properties of Neural Networks (Szegedy et al., ICLR 2014) - Uncovered the vulnerability of deep neural networks to adversarial examples, motivating the field of certified robustness. Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope (Wong and Kolter, ICML 2018) - Formulated certified defense training by bounding the convex outer adversarial polytope via linear programming duality. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (Katz et al., CAV 2017) - Introduced the Reluplex algorithm, extending the Simplex method to handle ReLU activation functions. Towards Fast Computation of Certified Robustness for ReLU Networks (Weng et al., ICML 2018) - Formulated the linear relaxation bounds (CROWN) that underpin many modern accelerated verifiers. Community Neural Verification Community - Portal hosting community forums, links to competitions, and collaborative projects. VNN-LIB - The standardized property specification language and network metadata standards for formal verification. Contributing Contributions are welcome! Please read the contributing guidelines first.