Formal Verification of Neural Certificates Done Dynamically

TL;DR

This paper introduces a lightweight runtime verification framework for neural certificates in control systems, enabling real-time safety assurance without exhaustive static analysis.

Contribution

It proposes a novel dynamic verification method that monitors neural certificates during deployment, addressing scalability issues of traditional static verification.

Findings

Effective real-time safety monitoring demonstrated in case study

Minimal computational overhead during deployment

Detects safety violations and incorrect certificates promptly

Abstract

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.