Formal Verification and Runtime Shielding for Safe Reinforcement Learning

Reinforcement learning enables agents to learn effective behaviours through interaction with their environment, but its exploratory nature makes it difficult to guarantee compliance with strict safety requirements. Runtime shielding addresses this problem by separating task optimization from safety enforcement, restricting the actions proposed by a learned policy according to a predefined safety specification. However, the resulting guarantees depend on the correctness of the software implementing the shield. This thesis presents a general methodology for constructing formally verified runtime shields for reinforcement learning. Lean~4 is used to express safety specifications, implement executable safety decision procedures, and formally prove their correctness within a common formal environment. The methodology is evaluated across four environments, including single-agent navigation, dynamic obstacles, adversarial agents, and multi-agent railway coordination in Flatland. These case studies demonstrate how different safety requirements can be addressed through a common construction process, from which recurring verification patterns for safe continuation, adversarial branching, and sequential reservation are identified. The results demonstrate that formal safety enforcement can be integrated with reinforcement learning without formally verifying the learning component itself. The resulting methodology provides a general framework for constructing independently verified runtime safety mechanisms while retaining the flexibility of reinforcement learning for task optimization.