# Shield Synthesis: Runtime Enforcement for Reactive Systems

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

## Key facts

- Cited by 42 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Jan 2015.

## Built on by (most cited first, 30 of 42)

- [Online Shielding for Reinforcement Learning](https://mlsanity.com/paper/2212.01861/) (2022)
- [Runtime Monitoring of Dynamic Fairness Properties](https://mlsanity.com/paper/2305.04699/) (2023)
- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Verification-Guided Shielding for Deep Reinforcement Learning](https://mlsanity.com/paper/2406.06507/) (2024)
- [Correct-by-Construction Runtime Enforcement in AI -- A Survey](https://mlsanity.com/paper/2208.14426/) (2022)
- [Shield Synthesis for LTL Modulo Theories](https://mlsanity.com/paper/2406.04184/) (2024)
- [Dynamic Shielding for Reinforcement Learning in Black-Box Environments](https://mlsanity.com/paper/2207.13446/) (2022)
- [Automata Learning meets Shielding](https://mlsanity.com/paper/2212.01838/) (2022)
- [Shielded Reinforcement Learning for Hybrid Systems](https://mlsanity.com/paper/2308.14424/) (2023)
- [Approximate Model-Based Shielding for Safe Reinforcement Learning](https://mlsanity.com/paper/2308.00707/) (2023)
- [Leveraging Approximate Model-based Shielding for Probabilistic Safety Guarantees in Continuous Environments](https://mlsanity.com/paper/2402.00816/) (2024)
- [Optimal Transport-Assisted Risk-Sensitive Q-Learning](https://mlsanity.com/paper/2406.11774/) (2024)
- [Efficient Shield Synthesis via State-Space Transformation](https://mlsanity.com/paper/2407.19911/) (2024)
- [Sovereign Assurance Boundary: Certificate-Bound Admission for Agentic Infrastructure](https://mlsanity.com/paper/2606.11632/) (2026)
- [What Can Be Enforced? A Theory of Certified Runtime Safety for Tool-Using Agents](https://mlsanity.com/paper/2607.22868/) (2026)
- [Safety Shielding under Delayed Observation](https://mlsanity.com/paper/2307.02164/) (2023)
- [Learning-Based Shielding for Safe Autonomy under Unknown Dynamics](https://mlsanity.com/paper/2410.07359/) (2024)
- [Neural Control and Certificate Repair via Runtime Monitoring](https://mlsanity.com/paper/2412.12996/) (2024)
- [Sovereign Execution Broker: Enforcing Certificate-Bound Authority in Agentic Control Planes](https://mlsanity.com/paper/2606.20520/) (2026)
- [Approximate Shielding of Atari Agents for Safe Exploration](https://mlsanity.com/paper/2304.11104/) (2023)
- [Shielded Deep Reinforcement Learning for Complex Spacecraft Tasking](https://mlsanity.com/paper/2403.05693/) (2024)
- [Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis](https://mlsanity.com/paper/2407.09348/) (2024)
- [ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems](https://mlsanity.com/paper/2511.02164/) (2025)
- [Semantic Quorum Assurance: Collective Certification for Non-Deterministic AI Infrastructure](https://mlsanity.com/paper/2606.08021/) (2026)
- [Think Smart, Act SMARL! Analyzing Probabilistic Logic Shields for Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2411.04867/) (2024)
- [Formal Verification of Neural Certificates Done Dynamically](https://mlsanity.com/paper/2507.11987/) (2025)
- [Safe Reinforcement Learning via Recovery-based Shielding with Gaussian Process Dynamics Models](https://mlsanity.com/paper/2602.12444/) (2026)
- [Easy-to-Use Shielding for Reinforcement Learning](https://mlsanity.com/paper/2606.03804/) (2026)
- [Compiling Sufficient Governance Context from Declared Losses and Reachable States: Exact Observation-Contract Synthesis with Cardinality and Cost Objectives](https://mlsanity.com/paper/2609.26016/) (2026)
- [MORTAR: A Model-based Runtime Action Repair Framework for AI-enabled Cyber-Physical Systems](https://mlsanity.com/paper/2408.03892/) (2024)

## Abstract (arXiv)

Scalability issues may prevent users from verifying critical properties of a complex hardware design. In this situation, we propose to synthesize a "safety shield" that is attached to the design to enforce the properties at run time. Shield synthesis can succeed where model checking and reactive synthesis fail, because it only considers a small set of critical properties, as opposed to the complex design, or the complete specification in the case of reactive synthesis. The shield continuously monitors the input/output of the design and corrects its erroneous output only if necessary, and as little as possible, so other non-critical properties are likely to be retained. Although runtime enforcement has been studied in other domains such as action systems, reactive systems pose unique challenges where the shield must act without delay. We thus present the first shield synthesis solution for reactive hardware systems and report our experimental results. This is an extended version of [5], featuring an additional appendix.