# A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 80 references that are in the map.
- First posted on arXiv 12 Sep 2023.

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

- [Control Barrier Function Based Quadratic Programs for Safety Critical Systems](https://mlsanity.com/paper/1609.06408/) (2016)
- [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)
- [The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systems](https://mlsanity.com/paper/1808.00924/) (2018)
- [Lyapunov-stable neural-network control](https://mlsanity.com/paper/2109.14152/) (2021)
- [Neural Certificates for Safe Control Policies](https://mlsanity.com/paper/2006.08465/) (2020)
- [Learning Lyapunov Functions for Hybrid Systems](https://mlsanity.com/paper/2012.12015/) (2020)
- [Learning Control Lyapunov Functions from Counterexamples and Demonstrations](https://mlsanity.com/paper/1804.05285/) (2018)
- [Learning Safe Neural Network Controllers with Barrier Certificates](https://mlsanity.com/paper/2009.09826/) (2020)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers](https://mlsanity.com/paper/2007.10865/) (2020)
- [High-order Barrier Functions: Robustness, Safety and Performance-Critical Control](https://mlsanity.com/paper/2104.00101/) (2021)
- [Learning Lyapunov Functions for Piecewise Affine Systems with Neural Network Controllers](https://mlsanity.com/paper/2008.06546/) (2020)
- [Counterexample Guided Synthesis of Switched Controllers for Reach-While-Stay Properties](https://mlsanity.com/paper/1505.01180/) (2015)
- [Counter-Example Guided Synthesis of Control Lyapunov Functions for Switched Systems](https://mlsanity.com/paper/1509.03688/) (2015)
- [Smooth Converse Lyapunov-Barrier Theorems for Asymptotic Stability with Safety Constraints and Reach-Avoid-Stay Specifications](https://mlsanity.com/paper/2009.04432/) (2020)
- [Controller Synthesis with Inductive Proofs for Piecewise Linear Systems: an SMT-based Algorithm](https://mlsanity.com/paper/1509.04623/) (2015)
- [Formal Synthesis of Lyapunov Neural Networks](https://mlsanity.com/paper/2003.08910/) (2020)
- [Formal controller synthesis for hybrid systems using genetic programming](https://mlsanity.com/paper/2003.14322/) (2020)
- [Counter-example guided inductive synthesis of control Lyapunov functions for uncertain systems](https://mlsanity.com/paper/2303.10024/) (2023)
- [Converse Theorems for Safety and Barrier Certificates](https://mlsanity.com/paper/1701.03948/) (2017)

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

- [Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems](https://mlsanity.com/paper/2405.06624/) (2024)
- [Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation](https://mlsanity.com/paper/2404.07956/) (2024)
- [Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models](https://mlsanity.com/paper/2311.09793/) (2023)
- [Two-Stage Learning of Stabilizing Neural Controllers via Zubov Sampling and Iterative Domain Expansion](https://mlsanity.com/paper/2506.01356/) (2025)
- [Safe and Reliable Training of Learning-Based Aerospace Controllers](https://mlsanity.com/paper/2407.07088/) (2024)
- [Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis](https://mlsanity.com/paper/2511.14755/) (2025)

## Abstract (arXiv)

An emerging branch of control theory specialises in certificate learning, concerning the specification of a desired (possibly complex) system behaviour for an autonomous or control model, which is then analytically verified by means of a function-based proof. However, the synthesis of controllers abiding by these complex requirements is in general a non-trivial task and may elude the most expert control engineers. This results in a need for automatic techniques that are able to design controllers and to analyse a wide range of elaborate specifications. In this paper, we provide a general framework to encode system specifications and define corresponding certificates, and we present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks to provide candidate control and certificate functions, whilst using SMT-solvers to offer a formal guarantee of correctness. We test our framework by developing a prototype software tool, and assess its efficacy at verification via control and certificate synthesis over a large and varied suite of benchmarks.