# SMC-ES: Automated synthesis of formally verified control policies

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Safe and constrained RL, one of 15 directions in Deep reinforcement learning methods.
- Builds on 18 of its 53 references that are in the map.
- First posted on arXiv 16 Jul 2026.

## Placed in

- Deep reinforcement learning methods / [Safe and constrained RL](https://mlsanity.com/deeprl/safe-and-constrained-rl/)

## Builds on (most cited first, 18 of 18)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Trust Region Policy Optimization](https://mlsanity.com/paper/1502.05477/) (2015)
- [Addressing Function Approximation Error in Actor-Critic Methods](https://mlsanity.com/paper/1802.09477/) (2018)
- [A Minimalist Approach to Offline Reinforcement Learning](https://mlsanity.com/paper/2106.06860/) (2021)
- [Deep Reinforcement Learning that Matters](https://mlsanity.com/paper/1709.06560/) (2017)
- [Sim-to-Real Transfer of Robotic Control with Dynamics Randomization](https://mlsanity.com/paper/1710.06537/) (2017)
- [Evolution Strategies as a Scalable Alternative to Reinforcement Learning](https://mlsanity.com/paper/1703.03864/) (2017)
- [Safe Learning in Robotics: From Learning-Based Control to Safe Reinforcement Learning](https://mlsanity.com/paper/2108.06266/) (2021)
- [Controlling Overestimation Bias with Truncated Mixture of Continuous Distributional Quantile Critics](https://mlsanity.com/paper/2005.04269/) (2020)
- [Safety-Gymnasium: A Unified Safe Reinforcement Learning Benchmark](https://mlsanity.com/paper/2310.12567/) (2023)
- [Diffusion Actor-Critic with Entropy Regulator](https://mlsanity.com/paper/2405.15177/) (2024)
- [Simple random search provides a competitive approach to reinforcement learning](https://mlsanity.com/paper/1803.07055/) (2018)
- [For SALE: State-Action Representation Learning for Deep Reinforcement Learning](https://mlsanity.com/paper/2306.02451/) (2023)
- [Empirical Design in Reinforcement Learning](https://mlsanity.com/paper/2304.01315/) (2023)
- [Deep Reinforcement Learning Versus Evolution Strategies: A Comparative Survey](https://mlsanity.com/paper/2110.01411/) (2021)
- [Distributional Soft Actor-Critic with Three Refinements](https://mlsanity.com/paper/2310.05858/) (2023)
- [Risk-Sensitive Reinforcement Learning with Exponential Criteria](https://mlsanity.com/paper/2212.09010/) (2022)

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

- [Safe and Robust Neural Policy Learning with Statistical Verification for Sim-to-Real Deployment in Robotics](https://mlsanity.com/paper/2608.06481/) (2026)
- [Micro Neural Policies for Safe Real-Time Robotic Control](https://mlsanity.com/paper/2610.08541/) (2026)

## Abstract (arXiv)

The deployment of autonomous cyber-physical systems in safety-critical environments requires closed-loop control strategies (i.e., policies) that are not only performant but also provably safe and robust. While learning-based methodologies such as Reinforcement Learning offer flexible and scalable approaches to automatically synthesize such controllers, they typically lack the formal guarantees necessary for safe deployment. To bridge this gap, we propose a novel simulation-based methodology to automatically synthesize policies with formal guarantees regarding performance, safety, and robustness specifications. Specifically, given a set of properties to verify, a confidence parameter δ and an allowable failure probability varepsilon, our method guarantees that the synthesized policy comes with a certificate: with confidence at least 1 - δ, the probability of encountering a scenario where the given properties are violated is at most varepsilon. We demonstrate the feasibility of our approach by developing SMC-ES, an algorithm that integrates Evolutionary Strategies with Statistical Model Checking-based verification. We evaluate SMC-ES on a suite of continuous control tasks using Gymnasium and Safety Gymnasium testbeds. Results show that, at the price of a sustainable increase in computational cost, our algorithm provides formal guarantees regarding performance, safety, and robustness specifications, while performing competitively against leading model-free Deep Reinforcement Learning (DRL) and Safe-DRL baselines.