TNODEV: Toolbox for Neural ODE Verification
TNODEV is a formal verifier for neural ODEs that combines reachability, falsification, and iterative refinement into one pipeline. It uses continuous-time mixed monotonicity for fast reachability and a loop with heuristics like MSIR to split uncertain states. This allows it to verify safety across pure ODEs, closed-loop systems, and general neural ODEs.