Anytime-Valid Runtime Monitoring of Learned Barrier Certificates

Zhipeng Cao; Taoran Wu; Weiru Cui; Luke Ong; Bai Xue

eess.SYOct 20, 2026

Anytime-Valid Runtime Monitoring of Learned Barrier Certificates

Authors: Zhipeng Cao, Taoran Wu, Weiru Cui, Luke Ong, Bai Xue

Organizations: Institute of Software, Chinese Academy of Sciences · School of Advanced Interdisciplinary Sciences, University of Chinese Academy of Sciences · University of Chinese Academy of Sciences · College of Computing and Data Science, Nanyang Technological University

Abstract

Learned barrier certificates provide a principled mechanism for establishing safety of stochastic systems, but their validity may deteriorate during deployment when the underlying dynamics differ from those used for training. We propose an anytime-valid runtime monitor that audits a learned barrier certificate using observed closed-loop trajectories. The monitor is intended to detect loss of statistical support for the deployed barrier condition; it does not by itself guarantee detection before unsafe entry or safety of a subsequent intervention. Specifically, the conditional barrier-drift condition is formulated as an episode-wise sequential hypothesis test, and observed barrier increments are transformed into a nonnegative test supermartingale, yielding finite-sample false-alarm control under arbitrary stopping times. Inspired by finite-horizon safety verification, we further introduce a deterministic temporal shaping of the monitoring boundary, making the monitor more conservative early in a prescribed deployment horizon while preserving anytime-validity. The monitor is designed to detect statistical evidence that the safety certificate is no longer consistent with the observed dynamics, rather than to predict unsafe entry. To assess the monitor empirically, we evaluate empirical alarm behavior under valid and invalid certificates. Code and data are available at https://github.com/FormalCert-AI/runtime-barrier-monitor.

Figures & tables

Figure 1: Overview of the proposed framework for anytime-valid monitoring of learned barrier certificates.

Valid certificates
		Direct		DAB
System	$K_{\max}\ln a$	$\rho_{\alpha}$	$\hat{p}^{\max}$	$\rho_{\alpha}$	$\hat{p}^{\max}$
System 1	0	0.00	4.80	0.00	0.90
	4	0.00	0.20	0.00	0.10
System 2	0	0.00	0.00	0.00	0.00
	4	0.00	0.00	0.00	0.00

Table 1: Runtime monitoring under valid and invalid certificates with

K_{\max}\ln a=0

and the default setting

K_{\max}\ln a=4

on the same runs.

\rho_{\alpha}

is the fraction of initial states with

\hat{p}_{i}>\alpha

and

\hat{p}^{\max}=\max_{i}\hat{p}_{i}

is the worst-case alarm rate.

N=10^{3}

initial states,

R=10^{3}

trajectories per initial state,

K_{\max}=400

\alpha=0.05

. All values are percentages. Figure 3 shows the full distribution of

\hat{p}

Figure 2: The trade-off between avoiding unnecessary alarms and detecting degradation promptly.

Appendix figures & tables7 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 3: Distribution of the alarm rate

\hat{p}_{i}

over the

N=10^{3}

initial states, Direct (left half) against DAB (right half), with the standard rule

K_{\max}\ln a=0

(top row) and the default

K_{\max}\ln a=4

(bottom row); the row below each axis holds the share of initial states with

\hat{p}_{i}=0

Figure 4: Effect of the patience parameter

a

on the DAB alarm rates and evidence for the invalid certificates.

Figure 5: Initial barrier value

B(x_{0})

and alarm rate: solid lines and filled markers for the standard rule

K_{\max}\ln a=0

, dashed lines and hollow markers for the default

K_{\max}\ln a=4

Betting rules	Bet $\lambda_{t}$	Alarm	Guar.
Direct	$1/B_{t}$	$M_{t}\geq\frac{a^{K_{\max}-t}}{\alpha}$	✓
Fraction mix.	$c/B_{t},\ c\in\mathcal{C}$	$\bar{M}_{t}\geq\frac{a^{K_{\max}-t}}{\alpha}$	✓
Absolute mix.	$\min\{\beta,1/B_{t}\},\ \beta\in\mathcal{A}_{j}$	$\bar{M}_{t}\geq\frac{a^{K_{\max}-t}}{\alpha}$	✓
DAB	Eq. 4	$M_{t}\geq\frac{a^{K_{\max}-t}}{\alpha}$	✓

Appendix

Table 2: Compared betting rules, all driven by the increments

\delta_{t}=B_{t}-B_{t-1}

. Guar.:

P_{H_{0}}(\tau\leq K_{\max}\mid x_{0})\leq\alpha

for every

x_{0}

(Theorem 1 ).

Valid certificates
	Direct		Fraction mix.		Absolute mix. $\mathcal{A}_{1}$		Absolute mix. $\mathcal{A}_{2}$		DAB
System	$\rho_{\alpha}$	$\hat{p}^{\max}$	$\rho_{\alpha}$	$\hat{p}^{\max}$	$\rho_{\alpha}$	$\hat{p}^{\max}$	$\rho_{\alpha}$	$\hat{p}^{\max}$	$\rho_{\alpha}$	$\hat{p}^{\max}$
System 1	0.00	0.20	0.00	0.50	0.00	0.00	0.00	0.00	0.00	0.10
System 2	0.00	0.00	0.00	0.00	0.00	0.00	0.00	0.00	0.00	0.00
Invalid certificates
System 2-input attack	17.90	100.00	11.30	100.00	0.00	0.00	0.00	1.20	79.90	81.50

Appendix

Table 3: Comparison with other monitors on the runs of Table 1 .

N=10^{3}

initial states,

R=10^{3}

trajectories per initial state,

K_{\max}=400

K_{\max}\ln a=4

\alpha=0.05

. All values are percentages.

Figure 6: Distribution of the alarm rates

\hat{p}_{i}

over the initial states for all monitors (

K_{\max}\ln a=4

Figure 7: Sensitivity to the horizon

K_{\max}

, DAB memory

\gamma

and DAB cap

U

Runtime Verification

Runtime verification checks executing systems against formal properties to detect, predict, or prevent violations.

See all 62 papers

Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems
May 4, 2026Miriam Kranzlmüller, Lukas Koller, Tobias Ladner +1Neural Network Verification Safety-Critical Control
Technical University of Munich, Germany · Ludwig-Maximilians-Universität in Munich, Germany
Stochastic Barrier Certificates in the Presence of Dynamic Obstacles
Apr 22, 2026Rayan Mazouz, Luca Laurenti, Morteza LahijanianControl Barrier Functions Dynamic Obstacle Avoidance
Dept. of Aerospace Eng. Sciences at University of Colorado Boulder, USA · Delft University of Technology, The Netherlands
Runtime Monitoring of Supermartingale Certificates
Oct 14, 2026Mirco Giacobbe, Thomas A. Henzinger, Konstantin Kueffner +2Runtime Verification
University of Birmingham · Institute of Science and Technology Austria · University of Oxford +2

May 4, 2026J/K move · Enter open · S save

Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems

Miriam Kranzlmüller, Lukas Koller, Tobias Ladner, Matthias Althoff

Technical University of Munich, Germany · Ludwig-Maximilians-Universität in Munich, Germany

Neural Network Verification Safety-Critical Control Formal Verification

Open paper AskPDF arXiv

Barrier certificates are scalar functions over the state space of dynamical systems that separate all unsafe states from all reachable states. The existence of a barrier certificate formally verifies the safety of the dynamical system. Recent approaches synthesize barrier certificates by iteratively training a neural network. In each iteration, the candidate is formally verified - if successful, the barrier certificate is found. Instead, we propose a set-based training approach that tightly integrates verification into training via a set-based loss function that soundly encodes all barrier certificate properties. A loss of zero formally proves the validity of the barrier certificate, collapsing the iterative training and verification into a single training procedure. Our experiments demonstrate that our set-based training approach scales well with the system dimension and naturally handles complex nonlinear dynamics.

Abstract

Runtime Verification

Explore similar work

Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems

Stochastic Barrier Certificates in the Presence of Dynamic Obstacles

Runtime Monitoring of Supermartingale Certificates