# Provably Safe Neural Network Controllers via Differential Dynamic Logic arXiv: https://arxiv.org/abs/2402.10998 ยท HTML: https://mlsanity.com/paper/2402.10998/ ## Key facts - Cited by 7 papers in the map (data through 14 Oct 2026). - Builds on 48 of its 111 references that are in the map. - First posted on arXiv 16 Feb 2024. ## Builds on (most cited first, 30 of 48) - [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017) - [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017) - [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018) - [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021) - [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020) - [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018) - [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022) - [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020) - [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019) - [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020) - [Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions](https://mlsanity.com/paper/2109.06697/) (2021) - [The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systems](https://mlsanity.com/paper/1808.00924/) (2018) - [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020) - [Learning Safe Multi-Agent Control with Decentralized Neural Barrier Certificates](https://mlsanity.com/paper/2101.05436/) (2021) - [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019) - [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023) - [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021) - [OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems](https://mlsanity.com/paper/2108.01220/) (2021) - [The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results](https://mlsanity.com/paper/2312.16760/) (2023) - [Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach](https://mlsanity.com/paper/2004.12273/) (2020) - [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023) - [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019) - [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021) - [Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1912.07084/) (2019) - [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021) - [Learning Lyapunov Functions for Hybrid Systems](https://mlsanity.com/paper/2012.12015/) (2020) - [DNNV: A Framework for Deep Neural Network Verification](https://mlsanity.com/paper/2105.12841/) (2021) - [Three Decades of Activations: A Comprehensive Survey of 400 Activation Functions for Neural Networks](https://mlsanity.com/paper/2402.09092/) (2024) - [Interpreting Neural Network Judgments via Minimal, Stable, and Symbolic Corrections](https://mlsanity.com/paper/1802.07384/) (2018) - [Verification of Non-Linear Specifications for Neural Networks](https://mlsanity.com/paper/1902.09592/) (2019) ## Built on by (most cited first, 7 of 7) - [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025) - [Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AI](https://mlsanity.com/paper/2406.11563/) (2024) - [Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control](https://mlsanity.com/paper/2411.18235/) (2024) - [Verification of Autonomous Neural Car Control with KeYmaera X](https://mlsanity.com/paper/2504.03272/) (2025) - [Proof-Carrying Neuro-Symbolic Code](https://mlsanity.com/paper/2504.12031/) (2025) - [VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification](https://mlsanity.com/paper/2605.07451/) (2026) - [Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision](https://mlsanity.com/paper/2507.22760/) (2025) ## Abstract (arXiv) While neural networks (NNs) have potential as autonomous controllers for Cyber-Physical Systems, verifying the safety of NN based control systems (NNCSs) poses significant challenges for the practical use of NNs, especially when safety is needed for unbounded time horizons. One reason is the intractability of analyzing NNs, ODEs and hybrid systems. To this end, we introduce VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): The first general approach that allows reusing control theory results for NNCS verification. By joining forces, we exploit the efficiency of NN verification tools while retaining the rigor of differential dynamic logic (dL). Based on provably safe control envelopes in dL, we derive specifications for the NN which is proven via NN verification. We show that a proof of the NN adhering to the specification is mirrored by a dL proof on the infinite-time safety of the NNCS. The NN verification properties resulting from hybrid systems typically contain nonlinear arithmetic and arbitrary logical structures while efficient NN verification merely supports linear constraints. To overcome this divide, we present Mosaic: An efficient, sound and complete verification approach for polynomial real arithmetic properties on piece-wise linear NNs. Mosaic partitions complex verification queries into simple queries and lifts off-the-shelf linear constraint tools to the nonlinear setting in a completeness-preserving manner by combining approximation with exact reasoning for counterexample regions. Our evaluation demonstrates the versatility of VerSAILLE and Mosaic: We prove infinite-time safety on the classical Vertical Airborne Collision Avoidance NNCS verification benchmark for two scenarios while (exhaustively) enumerating counterexample regions in unsafe scenarios. We also show that our approach significantly outperforms State-of-the-Art tools in closed-loop NNV.