# Neural Proofs for Sound Verification and Control of Complex Systems

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 24 of its 54 references that are in the map.
- First posted on arXiv 20 Dec 2025.

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

- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (2019)
- [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)
- [Automated Verification and Synthesis of Stochastic Hybrid Systems: A Survey](https://mlsanity.com/paper/2101.07491/) (2021)
- [Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions](https://mlsanity.com/paper/2301.01526/) (2023)
- [Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models](https://mlsanity.com/paper/2311.09793/) (2023)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)
- [StocHy: automated verification and synthesis of stochastic processes](https://mlsanity.com/paper/1901.10287/) (2019)
- [FAUST2: Formal Abstractions of Uncountable-STate STochastic processes](https://mlsanity.com/paper/1403.3286/) (2014)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Stochastic Omega-Regular Verification and Control with Supermartingales](https://mlsanity.com/paper/2405.17304/) (2024)
- [Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers](https://mlsanity.com/paper/2007.10865/) (2020)
- [Termination Analysis of Probabilistic Programs through Positivstellensatz's](https://mlsanity.com/paper/1604.07169/) (2016)
- [Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems](https://mlsanity.com/paper/2404.01769/) (2024)
- [Verification of general Markov decision processes by approximate similarity relations and policy refinement](https://mlsanity.com/paper/1605.09557/) (2016)
- [Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs](https://mlsanity.com/paper/1709.04037/) (2017)
- [Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems](https://mlsanity.com/paper/2210.05304/) (2022)
- [Safe Reach Set Computation via Neural Barrier Certificates](https://mlsanity.com/paper/2404.18813/) (2024)
- [Quantitative Supermartingale Certificates](https://mlsanity.com/paper/2504.05065/) (2025)
- [Supermartingale Certificates for Quantitative Omega-regular Verification and Control](https://mlsanity.com/paper/2505.18833/) (2025)
- [Symbolic control of stochastic systems via approximately bisimilar finite abstractions](https://mlsanity.com/paper/1302.3868/) (2013)
- [Aggregation and Control of Populations of Thermostatically Controlled Loads by Formal Abstractions](https://mlsanity.com/paper/1307.6716/) (2013)
- [Polynomial Probabilistic Invariants and the Optional Stopping Theorem](https://mlsanity.com/paper/1910.12634/) (2019)
- [Lexicographic Ranking Supermartingales with Lazy Lower Bounds](https://mlsanity.com/paper/2304.11363/) (2023)

## Abstract (arXiv)

This informal contribution presents an ongoing line of research that is pursuing a new approach to the construction of sound proofs for the formal verification and control of complex stochastic models of dynamical systems, of reactive programs and, more generally, of models of Cyber-Physical Systems. Neural proofs are made up of two key components: 1) proof rules encode requirements entailing the verification of general temporal specifications over the models of interest; and 2) certificates that discharge such rules, namely they are constructed from said proof rules with an inductive (that is, cyclic, repetitive) approach; this inductive approach involves: 2a) accessing samples from the model's dynamics and accordingly training neural networks, whilst 2b) generalising such networks via SAT-modulo-theory (SMT) queries that leverage the full knowledge of the models. In the context of sequential decision making problems over complex stochastic models, it is possible to additionally generate provably-correct policies/strategies/controllers, namely state-feedback functions that, in conjunction with neural certificates, formally attain the given specifications for the models of interest.