# Runtime Monitoring of Supermartingale Certificates

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 27 of its 44 references that are in the map.
- First posted on arXiv 14 Oct 2026.

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

- [Domain Randomization for Transferring Deep Neural Networks from Simulation to the Real World](https://mlsanity.com/paper/1703.06907/) (2017)
- [Sim-to-Real Transfer in Deep Reinforcement Learning for Robotics: a Survey](https://mlsanity.com/paper/2009.13303/) (2020)
- [Estimating means of bounded random variables by betting](https://mlsanity.com/paper/2010.09686/) (2020)
- [Game-theoretic statistics and safe anytime-valid inference](https://mlsanity.com/paper/2210.01948/) (2022)
- [Conformal Prediction for STL Runtime Verification](https://mlsanity.com/paper/2211.01539/) (2022)
- [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)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)
- [Stochastic Omega-Regular Verification and Control with Supermartingales](https://mlsanity.com/paper/2405.17304/) (2024)
- [On Continuous Monitoring of Risk Violations under Unknown Shift](https://mlsanity.com/paper/2506.16416/) (2025)
- [Termination Analysis of Probabilistic Programs through Positivstellensatz's](https://mlsanity.com/paper/1604.07169/) (2016)
- [Stochastic Invariants for Probabilistic Termination](https://mlsanity.com/paper/1611.01063/) (2016)
- [Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems](https://mlsanity.com/paper/2210.05304/) (2022)
- [Neural Continuous-Time Supermartingale Certificates](https://mlsanity.com/paper/2412.17432/) (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)
- [Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates](https://mlsanity.com/paper/2406.00826/) (2024)
- [Reach-Avoid Analysis for Polynomial Stochastic Differential Equations](https://mlsanity.com/paper/2208.10752/) (2022)
- [PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems](https://mlsanity.com/paper/2404.14804/) (2024)
- [Sound and Complete Proof Rules for Probabilistic Termination](https://mlsanity.com/paper/2404.19724/) (2024)
- [Diagnostic Runtime Monitoring with Martingales](https://mlsanity.com/paper/2407.21748/) (2024)
- [Neural Control and Certificate Repair via Runtime Monitoring](https://mlsanity.com/paper/2412.12996/) (2024)
- [A Hierarchy of Supermartingales for ω-Regular Verification](https://mlsanity.com/paper/2512.00270/) (2025)
- [Predictive Monitoring of Black-Box Dynamical Systems](https://mlsanity.com/paper/2412.16564/) (2024)
- [Formal Verification of Neural Certificates Done Dynamically](https://mlsanity.com/paper/2507.11987/) (2025)
- [Alignment Monitoring](https://mlsanity.com/paper/2508.00021/) (2025)
- [Complete ω-Regular Supermartingale Certificates](https://mlsanity.com/paper/2605.21134/) (2026)

## Abstract (arXiv)

Supermartingale certificates formally guarantee temporal properties of discrete and continuous-time stochastic dynamical systems. However, these guarantees rely on a mathematical model of the world, leaving a sim-to-real gap that can invalidate them for the deployed system. We formulate the runtime monitoring problem for supermartingale certificates, in which a monitor observes a single system trajectory and raises an alarm when there is sufficient statistical evidence that the supermartingale certificate has been violated during execution. We present an algorithm to automatically construct a monitor using betting-based sequential tests that bound the probability of ever raising a false alarm at a user-specified level. Within this betting framework, we formulate strategies that allow the monitor to exploit spatial regularity to improve detection power while preserving this statistical guarantee. We demonstrate the efficacy of our approach on supermartingale certificate benchmarks from the literature.