# Adaptive Shielding via Parametric Safety Proofs

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Feb 2025.

## Built on by (most cited first, 5 of 5)

- [Shields to Guarantee Probabilistic Safety in MDPs](https://mlsanity.com/paper/2605.10888/) (2026)
- [Efficient Dynamic Shielding for Parametric Safety Specifications](https://mlsanity.com/paper/2505.22104/) (2025)
- [Adaptive GR(1) Specification Repair for Liveness-Preserving Shielding in Reinforcement Learning](https://mlsanity.com/paper/2511.02605/) (2025)
- [Knowledge- and Gradient-Guided Reinforcement Learning for Parametrized Action Markov Decision Processes](https://mlsanity.com/paper/2607.12924/) (2026)
- [Adaptive Probabilistic Shielding by Learning MDPs for Safe Reinforcement Learning](https://mlsanity.com/paper/2608.19836/) (2026)

## Abstract (arXiv)

A major challenge to deploying cyber-physical systems with learning-enabled controllers is to ensure their safety, especially in the face of changing environments that necessitate runtime knowledge acquisition. Model-checking and automated reasoning have been successfully used for shielding, i.e., to monitor untrusted controllers and override potentially unsafe decisions, but only at the cost of hard tradeoffs in terms of expressivity, safety, adaptivity, precision and runtime efficiency. We propose a programming-language framework that allows experts to statically specify adaptive shields for learning-enabled agents, which enforce a safe control envelope that gets more permissive as knowledge is gathered at runtime. A shield specification provides a safety model that is parametric in the current agent's knowledge. In addition, a nondeterministic inference strategy can be specified using a dedicated domain-specific language, enforcing that such knowledge parameters are inferred at runtime in a statistically-sound way. By leveraging language design and theorem proving, our proposed framework empowers experts to design adaptive shields with an unprecedented level of modeling flexibility, while providing rigorous, end-to-end probabilistic safety guarantees.
