conference paper published yes Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000-0002-2985-7724 Konstantin Kueffner author 8121a2d0-dc85-11ea-9058-af578f3b45150000-0001-8974-2542 Zhengqi Yu author 20aa2ae8-f2f1-11ed-bbfa-8205053f13420000-0002-4993-773X ToHe department RV: Runtime Verification Vigilant Algorithmic Monitoring of Software project 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. Springer Nature2025Graz, Austria eng 0302-9743 1611-3349 2507.1198710.1007/978-3-032-05435-7_4 1608754-72 T. A. Henzinger, K. Kueffner, and E. Yu, “Formal verification of neural certificates done dynamically,” in <i>25th International Conference on Runtime Verification</i>, Graz, Austria, 2025, vol. 16087, pp. 54–72. Henzinger, Thomas A, Konstantin Kueffner, and Emily Yu. “Formal Verification of Neural Certificates Done Dynamically.” In <i>25th International Conference on Runtime Verification</i>, 16087:54–72. Springer Nature, 2025. <a href="https://doi.org/10.1007/978-3-032-05435-7_4">https://doi.org/10.1007/978-3-032-05435-7_4</a>. Henzinger, Thomas A., et al. “Formal Verification of Neural Certificates Done Dynamically.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 54–72, doi:<a href="https://doi.org/10.1007/978-3-032-05435-7_4">10.1007/978-3-032-05435-7_4</a>. T.A. Henzinger, K. Kueffner, E. Yu, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 54–72. Henzinger, T. A., Kueffner, K., &#38; Yu, E. (2025). Formal verification of neural certificates done dynamically. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 54–72). Graz, Austria: Springer Nature. <a href="https://doi.org/10.1007/978-3-032-05435-7_4">https://doi.org/10.1007/978-3-032-05435-7_4</a> Henzinger TA, Kueffner K, Yu E. 2025. Formal verification of neural certificates done dynamically. 25th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 16087, 54–72. Henzinger TA, Kueffner K, Yu E. Formal verification of neural certificates done dynamically. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:54-72. doi:<a href="https://doi.org/10.1007/978-3-032-05435-7_4">10.1007/978-3-032-05435-7_4</a> 210912026-01-29T16:03:01Z2026-02-16T11:53:25Z