# Formal Synthesis of Certifiably Robust Neural Lyapunov-Barrier Certificates

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Safe and constrained RL, one of 15 directions in Deep reinforcement learning methods.
- Builds on 26 of its 41 references that are in the map.
- First posted on arXiv 5 Feb 2026.

## Placed in

- Deep reinforcement learning methods / [Safe and constrained RL](https://mlsanity.com/deeprl/safe-and-constrained-rl/)

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

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Playing Atari with Deep Reinforcement Learning](https://mlsanity.com/paper/1312.5602/) (2013)
- [Reliable evaluation of adversarial robustness with an ensemble of diverse parameter-free attacks](https://mlsanity.com/paper/2003.01690/) (2020)
- [QT-Opt: Scalable Deep Reinforcement Learning for Vision-Based Robotic Manipulation](https://mlsanity.com/paper/1806.10293/) (2018)
- [Robust Adversarial Reinforcement Learning](https://mlsanity.com/paper/1703.02702/) (2017)
- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (2019)
- [Parseval Networks: Improving Robustness to Adversarial Examples](https://mlsanity.com/paper/1704.08847/) (2017)
- [Robust Deep Reinforcement Learning against Adversarial Perturbations on State Observations](https://mlsanity.com/paper/2003.08938/) (2020)
- [Deep Reinforcement Learning framework for Autonomous Driving](https://mlsanity.com/paper/1704.02532/) (2017)
- [Lipschitz-Margin Training: Scalable Certification of Perturbation Invariance for Deep Neural Networks](https://mlsanity.com/paper/1802.04034/) (2018)
- [Action Robust Reinforcement Learning and Applications in Continuous Control](https://mlsanity.com/paper/1901.09184/) (2019)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [Robust Reinforcement Learning on State Observations with Learned Optimal Adversary](https://mlsanity.com/paper/2101.08452/) (2021)
- [Globally-Robust Neural Networks](https://mlsanity.com/paper/2102.08452/) (2021)
- [Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions](https://mlsanity.com/paper/2109.06697/) (2021)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Robust Reinforcement Learning using Adversarial Populations](https://mlsanity.com/paper/2008.01825/) (2020)
- [Risk Averse Robust Adversarial Reinforcement Learning](https://mlsanity.com/paper/1904.00511/) (2019)
- [OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems](https://mlsanity.com/paper/2108.01220/) (2021)
- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees](https://mlsanity.com/paper/2210.05308/) (2022)
- [Safety Certification for Stochastic Systems via Neural Barrier Functions](https://mlsanity.com/paper/2206.01463/) (2022)
- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Robust Reinforcement Learning with Distributional Risk-averse formulation](https://mlsanity.com/paper/2206.06841/) (2022)

## Abstract (arXiv)

Neural Lyapunov and barrier certificates have recently been used as powerful tools for verifying the safety and stability properties of deep reinforcement learning (RL) controllers. However, existing methods offer guarantees only under fixed ideal unperturbed dynamics, limiting their reliability in real-world applications where dynamics may deviate due to uncertainties. In this work, we study the problem of synthesizing robust neural Lyapunov barrier certificates that maintain their guarantees under perturbations in system dynamics. We formally define a robust Lyapunov barrier function and specify sufficient conditions based on Lipschitz continuity that ensure robustness against bounded perturbations. We propose practical training objectives that enforce these conditions via adversarial training, Lipschitz neighborhood bound, and global Lipschitz regularization. We validate our approach in two practically relevant environments, Inverted Pendulum and 2D Docking. The former is a widely studied benchmark, while the latter is a safety-critical task in autonomous systems. We show that our methods significantly improve both certified robustness bounds (up to 4.6 times) and empirical success rates under strong perturbations (up to 2.4 times) compared to the baseline. Our results demonstrate effectiveness of training robust neural certificates for safe RL under perturbations in dynamics.