# Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates

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

## Key facts

- Cited by 16 papers in the map (data through 14 Oct 2026).
- Placed in Safe and constrained RL, one of 15 directions in Deep reinforcement learning methods.
- Builds on 56 of its 99 references that are in the map.
- First posted on arXiv 22 May 2024.

## Placed in

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

## Builds on (most cited first, 30 of 56)

- [Playing Atari with Deep Reinforcement Learning](https://mlsanity.com/paper/1312.5602/) (2013)
- [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)
- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (2019)
- [Safe Learning in Robotics: From Learning-Based Control to Safe Reinforcement Learning](https://mlsanity.com/paper/2108.06266/) (2021)
- [A Lyapunov-based Approach to Safe Reinforcement Learning](https://mlsanity.com/paper/1805.07708/) (2018)
- [Control Barrier Function Based Quadratic Programs for Safety Critical Systems](https://mlsanity.com/paper/1609.06408/) (2016)
- [Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances](https://mlsanity.com/paper/1709.07523/) (2017)
- [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)
- [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)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Learning Safe Multi-Agent Control with Decentralized Neural Barrier Certificates](https://mlsanity.com/paper/2101.05436/) (2021)
- [Reinforcement Learning for Safety-Critical Control under Model Uncertainty, using Control Lyapunov Functions and Control Barrier Functions](https://mlsanity.com/paper/2004.07584/) (2020)
- [Reachability Constrained Reinforcement Learning](https://mlsanity.com/paper/2205.07536/) (2022)
- [Safety and Liveness Guarantees through Reach-Avoid Reinforcement Learning](https://mlsanity.com/paper/2112.12288/) (2021)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [Learning Stability Certificates from Data](https://mlsanity.com/paper/2008.05952/) (2020)
- [Reach-Avoid Problems with Time-Varying Dynamics, Targets and Constraints](https://mlsanity.com/paper/1410.6445/) (2014)
- [Shield Synthesis: Runtime Enforcement for Reactive Systems](https://mlsanity.com/paper/1501.02573/) (2015)
- [Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees](https://mlsanity.com/paper/2206.01913/) (2022)
- [Fastened CROWN: Tightened Neural Network Robustness Certificates](https://mlsanity.com/paper/1912.00574/) (2019)
- [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)
- [Iterative Reachability Estimation for Safe Reinforcement Learning](https://mlsanity.com/paper/2309.13528/) (2023)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [Stabilizing Neural Control Using Self-Learned Almost Lyapunov Critics](https://mlsanity.com/paper/2107.04989/) (2021)
- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)

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

- [Verification-Guided Shielding for Deep Reinforcement Learning](https://mlsanity.com/paper/2406.06507/) (2024)
- [Shield Synthesis for LTL Modulo Theories](https://mlsanity.com/paper/2406.04184/) (2024)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretation](https://mlsanity.com/paper/2408.03915/) (2024)
- [Neural Continuous-Time Supermartingale Certificates](https://mlsanity.com/paper/2412.17432/) (2024)
- [Safe and Reliable Training of Learning-Based Aerospace Controllers](https://mlsanity.com/paper/2407.07088/) (2024)
- [A Review On Safe Reinforcement Learning Using Lyapunov and Barrier Functions](https://mlsanity.com/paper/2508.09128/) (2025)
- [Incremental Neural Network Verification via Learned Conflicts](https://mlsanity.com/paper/2603.12232/) (2026)
- [Proof-Carrying Neuro-Symbolic Code](https://mlsanity.com/paper/2504.12031/) (2025)
- [Formal Verification of Neural Certificates Done Dynamically](https://mlsanity.com/paper/2507.11987/) (2025)
- [The FABRIC Strategy for Verifying Neural Feedback Systems](https://mlsanity.com/paper/2603.08964/) (2026)
- [On Improving Deep Active Learning with Formal Verification](https://mlsanity.com/paper/2512.14170/) (2025)
- [A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems](https://mlsanity.com/paper/2601.08065/) (2026)
- [Formal Synthesis of Certifiably Robust Neural Lyapunov-Barrier Certificates](https://mlsanity.com/paper/2602.05311/) (2026)
- [Neural Network Verification using Partial Multi-Neuron Relaxation](https://mlsanity.com/paper/2605.30155/) (2026)
- [Mining Verdict Boundaries for Neural Network Verification](https://mlsanity.com/paper/2607.28954/) (2026)

## Abstract (arXiv)

Deep reinforcement learning (DRL) is a powerful machine learning paradigm for generating agents that control autonomous systems. However, the ``black box'' nature of DRL agents limits their deployment in real-world safety-critical applications. A promising approach for providing strong guarantees on an agent's behavior is to use Neural Lyapunov Barrier (NLB) certificates, which are learned functions over the system whose properties indirectly imply that an agent behaves as desired. However, NLB-based certificates are typically difficult to learn and even more difficult to verify, especially for complex systems. In this work, we present a novel method for training and verifying NLB-based certificates for discrete-time systems. Specifically, we introduce a technique for certificate composition, which simplifies the verification of highly-complex systems by strategically designing a sequence of certificates. When jointly verified with neural network verification engines, these certificates provide a formal guarantee that a DRL agent both achieves its goals and avoids unsafe behavior. Furthermore, we introduce a technique for certificate filtering, which significantly simplifies the process of producing formally verified certificates. We demonstrate the merits of our approach with a case study on providing safety and liveness guarantees for a DRL-controlled spacecraft.