# Formal Verification of Neural Certificates Done Dynamically

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 37 references that are in the map.
- First posted on arXiv 16 Jul 2025.

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

- [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)
- [Medical Image Analysis using Convolutional Neural Networks: A Review](https://mlsanity.com/paper/1709.02250/) (2017)
- [Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions](https://mlsanity.com/paper/2109.06697/) (2021)
- [Learning Certified Control using Contraction Metric](https://mlsanity.com/paper/2011.12569/) (2020)
- [Shield Synthesis: Runtime Enforcement for Reactive Systems](https://mlsanity.com/paper/1501.02573/) (2015)
- [SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems](https://mlsanity.com/paper/1808.07921/) (2018)
- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Exact Verification of ReLU Neural Control Barrier Functions](https://mlsanity.com/paper/2310.09360/) (2023)
- [Learning a Formally Verified Control Barrier Function in Stochastic Environment](https://mlsanity.com/paper/2403.19332/) (2024)
- [The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS](https://mlsanity.com/paper/2102.12981/) (2021)
- [Shield Model Predictive Path Integral: A Computationally Efficient Robust MPC Approach Using Control Barrier Functions](https://mlsanity.com/paper/2302.11719/) (2023)
- [SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions](https://mlsanity.com/paper/2410.20326/) (2024)
- [Neural Model Checking](https://mlsanity.com/paper/2410.23790/) (2024)
- [Neural Control and Certificate Repair via Runtime Monitoring](https://mlsanity.com/paper/2412.12996/) (2024)
- [Predictive Monitoring of Black-Box Dynamical Systems](https://mlsanity.com/paper/2412.16564/) (2024)

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

- [Runtime Monitoring of Supermartingale Certificates](https://mlsanity.com/paper/2610.19701/) (2026)

## Abstract (arXiv)

Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates.