# TNODEV: Toolbox for Neural ODE Verification

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 33 references that are in the map.
- First posted on arXiv 15 Jun 2026.

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

- [Neural Ordinary Differential Equations](https://mlsanity.com/paper/1806.07366/) (2018)
- [FFJORD: Free-form Continuous Dynamics for Scalable Reversible Generative Models](https://mlsanity.com/paper/1810.01367/) (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)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [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)
- [Integrating Expert ODEs into Neural ODEs: Pharmacology and Disease Progression](https://mlsanity.com/paper/2106.02875/) (2021)
- [On The Verification of Neural ODEs with Stochastic Guarantees](https://mlsanity.com/paper/2012.08863/) (2020)
- [SurvLatent ODE : A Neural ODE based time-to-event model with competing risks for longitudinal data improves cancer-associated Venous Thromboembolism (VTE) prediction](https://mlsanity.com/paper/2204.09633/) (2022)
- [Reachability Analysis of a General Class of Neural Ordinary Differential Equations](https://mlsanity.com/paper/2207.06531/) (2022)
- [TIRA: Toolbox for Interval Reachability Analysis](https://mlsanity.com/paper/1902.05204/) (2019)
- [GoTube: Scalable Stochastic Verification of Continuous-Depth Models](https://mlsanity.com/paper/2107.08467/) (2021)
- [On the Forward Invariance of Neural ODEs](https://mlsanity.com/paper/2210.04763/) (2022)
- [Lagrangian Reachtubes: The Next Generation](https://mlsanity.com/paper/2012.07458/) (2020)
- [Bridging Neural ODE and ResNet: A Formal Error Bound for Safety Verification](https://mlsanity.com/paper/2506.03227/) (2025)
- [Mixed Monotonicity Reachability Analysis of Neural ODE: A Trade-Off Between Tightness and Efficiency](https://mlsanity.com/paper/2510.17859/) (2025)
- [Verifying Safety of Neural Networks from Topological Perspectives](https://mlsanity.com/paper/2306.15403/) (2023)

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

- [Robustness Verification of an Autonomous Underwater Vehicle-based Plankton Classifier](https://mlsanity.com/paper/2607.04453/) (2026)

## Abstract (arXiv)

Neural ordinary differential equations (neural ODE) gained attention in safety critical settings such as continuous-time controllers for cyber-physical systems and classifiers integrated into automated decision pipelines, raising the question whether their behavior can be formally verified. Existing tools dedicated to neural ODE provide only a single reachability call without iterative input-set refinement, limiting the precision of their verdicts to whatever one reachability call can deliver. We present TNODEV, the first formal verifier for neural ODE that integrates a falsification checker, a fast interval-based reachability backend based on continuous-time mixed monotonicity, a verification and refinement loop with three input-set splitting heuristics, and a parallel scheduler in a single end-to-end pipeline. TNODEV supports safe-set inclusion verification on pure neural ODE, neural ODE in closed loop with a neural network controller and general neural ODE (GNODE), with the safe set specified either as an interval or as the half-space intersection induced by a target classification label. We evaluate TNODEV on a range of benchmarks across safe-set inclusion and classification-robustness properties, including a direct reachability comparison against NNV 2.0 and CORA and a verification comparison against NNV 2.0 on MNIST general neural ODE classifiers.