Paper deep dive
LyEvO: Lyapunov-Guided Evolutionary Optimization for Safe and Robust Sim-to-Real Policy Learning
Riccardo Curcio, Hongpeng Cao, Marco Caccamo
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 93%
Last extracted: 8/10/2026, 2:27:56 AM
Summary
The paper introduces LyEvO, a framework for safe and robust sim-to-real policy learning that combines constrained Evolutionary Optimization with Statistical Model Checking (SMC) and Lyapunov-based stability analysis. It iteratively expands a stability region to formally verify policy safety and performance, demonstrated on Cartpole and 3D Quadrotor benchmarks.
Entities (11)
Relation Signals (8)
LyEvO → evaluatedon → Cartpole
confidence 95% · We evaluate LyEvO on Cartpole and 3D Quadrotor benchmarks
LyEvO → evaluatedon → 3D Quadrotor
confidence 95% · We evaluate LyEvO on Cartpole and 3D Quadrotor benchmarks
LyEvO → uses → Lyapunov analysis
confidence 95% · LyEvO uses Lyapunov analysis to compute an initial candidate stability region.
LyEvO → uses → Evolutionary Optimization
confidence 95% · LyEvO, a physics-grounded framework that combines constrained Evolutionary Optimization
LyEvO → uses → Statistical Model Checking
confidence 95% · combines constrained Evolutionary Optimization and Statistical Model Checking (SMC)-based verification
Riccardo Curcio → affiliatedwith → Sapienza University of Rome
confidence 90% · Riccardo Curcio is with the Department of Computer Science, Sapienza University of Rome
Hongpeng Cao → affiliatedwith → Technical University of Munich
confidence 90% · Hongpeng Cao and Marco Caccamo are with the School of Engineering and Design, Technical University of Munich
Marco Caccamo → affiliatedwith → Technical University of Munich
confidence 90% · Hongpeng Cao and Marco Caccamo are with the School of Engineering and Design, Technical University of Munich
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Training controllers that are safe and robust in simulation, and systematically assessing their readiness for real-world deployment, remain key challenges in sim-to-real transfer. To address this, we propose LyEvO, a physics-grounded framework that combines constrained Evolutionary Optimization and Statistical Model Checking (SMC)-based verification with Lyapunov-based stability analysis. Leveraging prior knowledge of the system dynamics, LyEvO uses Lyapunov analysis to compute an initial candidate stability region. An iterative loop then uses operational scenarios drawn from this region to jointly optimize and statistically verify a policy, and subsequently expands the region's boundaries based on the verification outcome. This integrated procedure provides a practical criterion for assessing deployment readiness. We evaluate LyEvO on Cartpole and 3D Quadrotor benchmarks through extensive simulations and targeted real-world experiments, demonstrating safe and robust sim-to-real transfer.
Tags
Links
- Source: https://arxiv.org/abs/2608.06481v1
- Canonical: https://arxiv.org/abs/2608.06481v1
Trouble viewing inline? Open PDF directly →
Full Text
53,342 characters extracted from source content.
Expand or collapse full text
LyEvO: Lyapunov-Guided Evolutionary Optimization for Safe and Robust Sim-to-Real Policy Learning Riccardo Curcio1,†, Hongpeng Cao2,†, Marco Caccamo2 † These authors contributed equally to this work.1 Riccardo Curcio is with the Department of Computer Science, Sapienza University of Rome, via Salaria 113, 00198 Rome, Italy2 Hongpeng Cao and Marco Caccamo are with the School of Engineering and Design, Technical University of Munich, Boltzmannstraße 15, 85748 Garching b. München, Germany Abstract Training controllers that are safe and robust in simulation, and systematically assessing their readiness for real-world deployment, remain key challenges in sim-to-real transfer. To address this, we propose LyEvO, a physics-grounded framework that combines constrained Evolutionary Optimization and Statistical Model Checking (SMC) -based verification with Lyapunov-based stability analysis. Leveraging prior knowledge of the system dynamics, LyEvO uses Lyapunov analysis to compute an initial candidate stability region. An iterative loop then uses operational scenarios drawn from this region to jointly optimize and statistically verify a policy, and subsequently expands the region’s boundaries based on the verification outcome. This integrated procedure provides a practical criterion for assessing deployment readiness. We evaluate LyEvO on Cartpole and 3D Quadrotor benchmarks through extensive simulations and targeted real-world experiments, demonstrating safe and robust sim-to-real transfer. I Introduction Learning control policies in simulation has emerged as a powerful paradigm for controller synthesis, demonstrating remarkable performance across a wide range of robotic tasks [1]. However, policies trained in simulation may be unsafe or unreliable in the real world due to modeling errors and/or unseen operational conditions, a phenomenon commonly known as the sim-to-real gap [2]. For real-world robotic applications, this raises two fundamental challenges: learning controllers that satisfy safety constraints while remaining robust to real-world uncertainties, and systematically assessing their safe operating region before deployment. I-A Motivation Existing work primarily addresses these challenges through two main paradigms: safe reinforcement learning [3] and robust reinforcement learning [4]. The former embeds stability or safety requirements directly into the policy optimization process, while the latter improves resilience through adversarial training, worst-case optimization, and broader simulation exposure [5]. However, these methods typically offer no formal guarantees regarding safety, primarily due to a lack of systematic verification across diverse operating scenarios. Without such assessment, success during training fails to characterize where the learned controller remains safe or with what confidence. Complementary approaches assess and improve deployment readiness through formal verification [6], simulation-based falsification [7], and runtime safety monitoring [8]. However, they are typically applied to a fixed policy after training, leaving the resulting safety evidence disconnected from the policy optimization process. In this work, we propose a method to bridge the gap between safe policy learning and deployment readiness by using a Lyapunov-based stability region to guide optimization and formally verify the learned controller. I-B Related Work I-B1 Safe Learning A large body of work improves safety during learning by incorporating safety requirements into the objective functions. Representative approaches include constrained policy optimization [9] and Lyapunov-based reward designs [10, 11]. Another direction integrates a safe policy prior with a Deep Reinforcement Learning (DRL) policy, allowing them to work collaboratively toward high task performance while improving runtime safety. Recent frameworks have explored this idea through policy-prior-aided training [12, 13]. However, these methods are typically evaluated only in few scenarios, leaving robustness to unseen disturbances and model uncertainties insufficiently characterized [14]. I-B2 Robust Training For robust policy training, Domain Randomization (DR) exposes policies to diverse simulated environments by varying physical parameters, disturbances, and task conditions [5]. While a sufficiently rich simulation distribution can improve real-world generalization, overly broad randomization may introduce unsolvable or uninformative scenarios, increasing training variance and degrading performance [15]. Curriculum-based methods mitigate this issue by progressively expanding the training distribution or selecting informative contexts [16, 15], whereas robust reinforcement learning explicitly optimizes against adversarial or worst-case uncertainties [4, 17]. Nevertheless, selecting informative randomization ranges, task variations, and initial conditions remains problem-dependent, motivating more systematic sampling for training and pre-deployment assessment. I-B3 Policy Verification Formal verification methods analyze trained neural policies under prescribed perturbation models and seek to establish properties such as local robustness, reachability, or constraint satisfaction [6, 18]. These methods can provide rigorous guarantees, but their applicability often depends on the network architecture, system model, and the complexity of the considered state and perturbation sets [18]. In contrast, simulation-based testing and falsification methods evaluate closed-loop behavior by searching for counterexamples or safety-violating trajectories. Existing approaches [19, 20] commonly employ temporal-logic specifications, adaptive scenario generation, or Statistical Model Checking (SMC) . These methods are generally more flexible and scalable to nonlinear systems, but their conclusions depend strongly on the representativeness and coverage of the sampled operating conditions. Moreover, they are typically applied post-training, providing limited direct guidance for learning safe policies, although recent approaches have begun integrating simulation-based verification into policy synthesis [21]. I-C Contribution To bridge the gap between safe policy learning and deployment readiness, we propose LyEvO, a physics-grounded framework that iteratively couples constrained Evolutionary Optimization, SMC -based verification, and Lyapunov-based stability region expansion. This closed-loop procedure optimizes controller performance while progressively enlarging its verified stability region. The main contributions are as follows: • The LyEvO Framework: Given a task specification (i.e., objective and constraint functions) and an initial Lyapunov candidate stability region, we develope a method to systematically expand this domain. At each step, we run a counterexample-driven loop combining constrained Evolution Strategy (ES) with SMC -based verification [21] to optimize a policy over the current region while statistically guaranteeing its safety and performance lower bound. Based on the outcome, we progressively expand the region, driving the policy to be safe and robust across broader conditions. Upon convergence, the resulting policy comes with a formal certificate: with at least 1−δ1-δ confidence, the probability of encountering a scenario within the expanded region where the policy violates safety constraints or achieves a performance below the claimed lower bound is at most ε . Crucially, these guarantees encompass safety (avoiding unsafe states), performance lower bound (guaranteeing task proficiency), and robustness (maintaining these properties under uncertainty). • Simulation Validation: We evaluate LyEvO on cartpole and 3D quadrotor benchmarks through extensive simulations, demonstrating that our framework significantly expands the stability region compared to several DRL baselines. • Real-World Deployment: We deploy on hardware only policies that are either mathematically certified (i.e., Linear Matrix Inequality (LMI) -based policies) or successfully verified via SMC . Through real-world experiments under both nominal and disturbed conditions, we showcase LyEvO’s superior robustness, demonstrating that our verified policies reliably translate to physical reality. We provide video demonstration at the following link. I Background We use ℝR to denote the set of real numbers. For x∈ℝn x ^n, xix_i denotes its i-th component, and vector inequalities are interpreted component-wise, i.e., a≤b a≤ b means ai≤bia_i≤ b_i for all i∈1,…,ni∈\1,…,n\. The vectors in ℝnR^n with all components equal to 0 and 11 are denoted by (n)0_(n) and (n)1_(n), respectively. Let =ℕT=N denote the discrete time set. A signal ∈z ^T assigns each t∈t a value zt∈z_t . For a random variable X, x∼Xx\, \,X denotes a realization of X, and Δ(X) (X) the space of all probability distributions over X. Furthermore, Pr(E) (E ) denotes the probability that a logical predicate or event E holds true. I-A MDP We formulate the robotic control problem as a sequential decision-making process between an agent and its environment, modeled as a Markov decision process (MDP). An MDP is defined by the tuple (,,R,P,γr,ρ0)(S,A,R,P, _r, _0), comprising a state space ⊆ℝnS ^n (n>0n>0), an action space ⊆ℝmA ^m (m>0m>0), a reward function R:×→ℝR:S×A×S , a transition kernel P:×→Δ()P:S×A→ (S), a discount factor γr∈[0,1) _r∈[0,1), and an initial state distribution ρ0∈Δ() _0∈ (S). Given an initial state 0∼ρ0 s_0 _0, at each time step t∈t the agent observes its state t∈ s_t , selects an action t∈ a_t according to a policy π (deterministic, π:→π:S , or stochastic, π:→Δ()π:S→ (A)), transitions to the next state t+1∼P(⋅∣t,t) s_t+1 P(· s_t, a_t), and receives the reward rt=R(t,t,t+1)r_t=R ( s_t, a_t, s_t+1 ). In this work, we assume the stochastic transition kernel P is induced by a deterministic discrete-time dynamics function :×→ f:S×A×W subject to an unknown disturbance, t+1=(t,t,t),t∈,t∈,t∈ s_t+1= f ( s_t, a_t, w_t ), s_t , a_t , w_t (1) where ⊆ℝqW ^q (q>0)(q>0) denotes the set of admissible disturbances, including modeling errors and external perturbations. Building on this, we define an operational scenario (0,) ( s_0, w ) as a joint realization of an initial state 0 s_0, sampled uniformly from a candidate region Ω⊆ (cf. 5), and a disturbance sequence w generated by discrete-time stochastic process W taking values in the disturbance set W. Letting ρc=((Ω),) _c=(U( ),W) denote their joint distribution (with (Ω)U( ) denoting the uniform distribution across states in Ω ), we write (0,)∼ρc ( s_0, w )\, \, _c for a scenario sampled from this distribution. With a slight abuse of notation, we instead denote with (0,)∈ρc ( s_0, w )∈ _c a scenario entailed by ρc _c. Finally, because our focus is on safety-critical applications, we introduce a set of hard constraint functions C=ci:×→ℝi=1zC=\c_i:S×A×S \_i=1^z (z>0z>0), where the i-th constraint is satisfied at time step t∈t whenever ci(t,t,t+1)≤0c_i ( s_t, a_t, s_t+1 )≤ 0. The goal of the agent is to determine a control policy that maximizes the expected cumulative reward while strictly satisfying these safety constraints under any operational scenario (0,)∈ρc ( s_0, w )∈ _c. Throughout the remainder of this work, we model a policy πθ _θ as a Neural Network (N) parameterized by θ∈ℝdθ ^d (d>0d>0). I-B Learning-based Controller Synthesis I-B1 Deep Reinforcement learning Deep Reinforcement Learning (DRL) for continuous-control problems commonly adopts an actor–critic architecture [22], in which an actor network πθ _θ represents the policy and a critic network Ψϕπθ _φ _θ estimates its long-term performance. The critic provides the learning signal used to update the actor. Actor–critic methods generally optimize an algorithm-specific surrogate objective of the form maxθℒπθ=∼ρπθ,∼πθ(⋅∣)[ℒ(,,πθ,Ψϕπθ)], _θL_ _θ=E_ s ρ _θ, a _θ(· s)[L( s, a, _θ, _φ _θ)], where ρπθρ _θ denotes the state distribution induced by the current policy, and ℒL is an algorithm-specific actor objective constructed from a critic estimate. Depending on the algorithm, the critic may represent an action-value, state-value, or advantage function. In practice, the expectation is estimated from on-policy trajectories or transitions sampled from a replay buffer. In safe RL, safety and robustness can be incorporated into ℒL through reward penalties [23], constrained optimization [9], or enforced at runtime by supervisory mechanisms that override unsafe actions [8]. I-B2 Evolution Strategies Evolution Strategy (ES) algorithms [24] are population-based Black Box Optimization (BBO) methods that evolve a distribution over candidate solutions without backpropagating gradients. To solve policy synthesis problems, ES evaluates a candidate policy πθ _θ using trajectory-level metrics over a finite horizon H∈H . As this finite horizon removes the need for temporal discounting [25], it computes the undiscounted cumulative reward: J(πθ,0,,H)=∑t=0H−1R(t,πθ(t),t+1)J ( _θ, s_0, w,H )= _t=0^H-1R ( s_t, _θ( s_t), s_t+1 ) and the cumulative constraint violations C(πθ,0,,H)=[∑t=0H−1max(0,cj(t,πθ(t),t+1))]j=1z,C ( _θ, s_0, w,H )= [ _t=0^H-1 (0,c_j( s_t, _θ( s_t), s_t+1)) ]_j=1^z, where, under a scenario (0,)∼ρc ( s_0, w )\, \, _c, the underlying state sequence evolves according to the system dynamics t+1=(t,πθ(t),t) s_t+1= f ( s_t, _θ( s_t), w_t ) as in Eq. (1). To optimize the policy, gradient-based ES approaches [25] estimate the gradient by evaluating N random policy perturbations. This process relies on an exploration noise scale σ>0σ>0 and N independent Gaussian perturbation vectors ζi∼((d),(d×d)) __i\, \, N ( [b]0_(d), [b] I_(d× d) ) for i=1,…,Ni=1,…,N. Each perturbation yields a perturbed policy πθi=πθ+σζi _ _i= _θ+σ __i. These N candidate policies are then evaluated on N independently sampled operational scenarios (0i,i)∼ρc( s_0^i, w^i)\, \, _c. We define Jπθi=J(πθi,0i,i,H)J_ _ _i=J ( _ _i, s_0^i, w^i,H ) and Cπθi=C(πθi,0i,i,H)C_ _ _i=C ( _ _i, s_0^i, w^i,H ) as the resulting cumulative reward and constraint violation, respectively. Following [25, 21], the gradient of the constrained objective can then be estimated as: ∇^θℒπθ=1Nσ∑i=1Nℒ(Jπθi,Cπθi)ζi, ∇_θL_ _θ= 1Nσ _i=1^NL (J_ _ _i,C_ _ _i ) __i, (2) where ℒL represents a fitness function (e.g., an augmented Lagrangian [26]) designed to combine the objective function with the satisfaction of the constraints. Formal verification Recent algorithmic variants, such as SMC-ES [21], bridge the gap between learning-based control synthesis and formal verification by directly returning policies equipped with formal statistical guarantees. SMC-ES achieves its guarantees through a counterexample-guided loop: it optimizes a policy using an ES -based algorithm over a finite set of sampled scenarios and then verifies it via Statistical Model Checking (SMC) . Whenever verification fails, the identified counterexamples are permanently appended to the training scenario set and the optimization restarts. We abstract this algorithm as a subroutine SMC-ES(,ρc,(R,C),πθ,H,δ,ε) SMC-ES( f, _c,(R,C), _θ,H,δ, ) that takes as input system dynamics f, an operational scenario distribution ρc _c, reward RR and constraint functions C, an initialized policy πθ _θ and an evaluation horizon H. Upon termination, SMC-ES() SMC-ES ( ) outputs the verified solution pair (πθ∗,β∗)( _θ^*,β^*) formalized below. Proposition 1 (Adapted from [21]). Given a confidence level δ∈(0,1]δ∈(0,1] and an allowable failure probability ε∈(0,1] ∈(0,1], the solution pair (πθ∗,β∗)( _θ^*,β^*) returned by SMC-ES(,ρc,(R,C),πθ,H,δ,ε) SMC-ES( f, _c,(R,C), _θ,H,δ, ) guarantees that, with confidence at least 1−δ1-δ, the following holds: Pr(0,)∼ρc(J(πθ∗,0,,H)<β∗⏞Performance violation∨C(πθ∗,0,,H)>(z)⏟Safety violation)≤ε. _ ( s_0, w )\, \, _c ( array[]c J ( _θ^*, s_0, w,H )<β^*^Performance violation\\[8.61108pt] \\[4.30554pt] C ( _θ^*, s_0, w,H )>0_(z)_Safety violation array )≤ . I Lyapunov-Guided Policy Optimization In this section, we present a framework to systematically expand and formally verify a policy’s stability region under safety and performance guarantees. I-A Stability region estimation In robotics, safety can be approached through stability by identifying the set of states from which the system can recover and converge to the desired state while satisfying prescribed constraints. This set is commonly characterized as a stability region, or region of attraction [27]. A larger certified stability region therefore corresponds to a broader range of initial conditions from which safe recovery can be guaranteed, indicating greater robustness and recovery capability. Motivated by this, we combine Lyapunov-based stability analysis with learning-based policy synthesis. Following standard Safe DRL practice [9], we promote stabilizing behavior through constrained objective maximization. However, rather than only optimizing an expected objective, we provide formal guarantees on safety and performance lower bound while progressively expanding the verified stability region. To realize this objective, we initialize the procedure using a model-based Lyapunov stability region Ω as a feasible initial candidate [28]. Exploiting its dynamics-informed geometry allows us to guide the region’s expansion and efficiently filter out physically infeasible scenarios. Figure 1: Illustration of the initial and enlarged Cartpole stability regions in a 2D projection, where sampled states with larger Lyapunov values lie closer to the region boundary. We construct Ω from a linear model prior using Lyapunov’s direct method while accounting for the prescribed state and input constraints. Specifically, we decompose the nonlinear dynamics as t+1 s_t+1 =t+t⏟known linear prior+′(t,t,t)⏟unknown residual dynamics, = A s_t+B a_t_known linear prior+ f ( s_t, a_t, w_t )_unknown residual dynamics, (3) where ′ f captures the nonlinearities, model mismatch, and disturbance effects not represented by the linear prior. For the initial synthesis, we parametrize a linear state feedback, t=t a_t=F s_t, and consider the nominal closed-loop system obtained by neglecting the residual: t+1 s_t+1 =¯t, = A s_t, ¯ A ≔+. +BF. (4) We parameterize the initial candidate stability region as ellipsoidal set Ω≔∈|⊤≤1,≻0. \ s \; |\; s P s≤ 1 \, 0. (5) For the quadratic Lyapunov function V()=⊤V( s)= s P s, the discrete-time Lyapunov condition ¯⊤¯−≺0 A P A-P 0 guarantees asymptotic stability of the nominal closed loop and positive invariance of Ω . The controller gain F and Lyapunov matrix P are obtained by jointly enforcing the Lyapunov condition above and the prescribed state and input constraints. Using standard changes of variables, these conditions can be expressed as LMIs and solved using convex optimization [29]. Starting from Ω , we progressively expand the region by enlarging it along its principal directions. Specifically, for the eigendecomposition =diag(λ1,…,λn)⊤, =Udiag( _1,…, _n)U , (6) the columns of U define the principal directions of Ω , while the corresponding semi-axis lengths are 1/λi1/ _i. Fig. 1 illustrates the sampled states, the initial region, and the final enlarged region for the Cartpole system in a two-dimensional projection. I-B Problem statement We formalize our Lyapunov-guided Safe and Robust policy design problem as follows. Definition 1. A Lyapunov-guided Safe and Robust policy design problem is a tuple Γ=(,ρc,(R,C),d,H,δ,ε) =( f, _c,(R,C),d,H,δ, ), where: • f is a discrete-time dynamical system as in 1. • ρc=((Ω),) _c=(U( ),W) is the initial scenario distribution, where Ω corresponds to the initial region as in 5 and W is a discrete-time stochastic process taking values in the disturbance set ⊆ℝqW ^q. • (R,C)(R,C) are reward and constraint functions. • d is the dimension of the policy parameter space ℝdR^d. • H∈H is a time horizon. This tuple formulates the following bilevel optimization problem: min ∑i=1nlog(γi) _i=1^n ( _i) (7) s.t. =diag(γ1λ1,…,γnλn)⊤, _ γ=Udiag( _1 _1,…, _n _n)U , Ω=∈|⊤≤1, _ γ= \ s \; |\; s P_ γ s≤ 1 \, ρc′=((Ω),), _c =(U( _ γ),W), min≤(n) γ_ ≤ γ 1_(n) (8) (θ,β)∈argmaxθ′∈ℝd,β′∈ℝβ′|J(πθ′,0,,H)≥β′,C(πθ′,0,,H)=(z),∀(0,)∈ρc′ (θ,β)∈ θ ^d,β arg\,max \β \; |\; aligned &J ( _θ , s_0, w,H )≥β ,\\ &C ( _θ , s_0, w,H )=0_(z),\\ &∀ ( s_0, w )∈ _c aligned \ For every feasible solution (,θ,β)( γ,θ,β) to the problem above, with induced expanded region Ω _ γ and scenario distribution ρc′=((Ω),) _c =(U( _ γ),W), the corresponding closed-loop system employing policy πθ _θ under dynamics 1 exhibits strictly safe and robust behavior across all scenarios (0,)∈ρc′ ( s_0, w )∈ _c . That is, it systematically satisfies all safety constraints (incurring a cumulative violation cost of (z)0_(z)) while guaranteeing a worst-case cumulative reward of β. definizione 1 formulates a bilevel optimization problem coupling geometric expansion and robust control: the outer level maximizes the volume of the stability region by minimizing the scaling factors γi _i, while the inner level maximizes the worst-case cumulative reward β of a strictly safe policy over all scenarios within that region. Minimizing the objective ∑i=1nlog(γi) _i=1^n ( _i) directly controls det() (P_ γ), thus maximizing the ellipsoid volume while preserving the principal directions of P. To keep the expanded region within state constraints (e.g., maximum positions or velocities), the lower bound vector min γ_ is precomputed analytically: each component γmin,i _ ,i defines the maximum allowable expansion along a principal axis (holding others fixed at 1) before the ellipsoid touches the nearest state boundary. This problem is computationally intractable in general, as even the inner worst-case maximization problem is undecideable. In sezione IV, we introduce LyEvO, a practical algorithm to efficiently approximate its solution. IV Algorithm design At a high level, LyEvO alternates between an outer region-expansion loop and an inner policy-search and verification loop (Algoritmo 1). First, the subroutine SMC-ES() SMC-ES ( ) is invoked to synthesize a formally verified policy over the initial candidate region Ω with all scaling factors γ set to 1. If a feasible solution is found, the outer loop begins progressively enlarging Ω _ γ. To bypass the intractability of an exact global search, this outer loop relies on a greedy heuristic that isolates and expands one dimension at a time, scaling each step proportionally to a fixed step size and available expansion headroom. For each proposed expansion Ω _ γ, the inner loop uses the SMC-ES() SMC-ES ( ) subroutine (sezione I-B2) to re-optimize and formally verify the policy against the new operational scenario distribution dictated by Ω _ γ. Further implementation details of SMC-ES are provided in [21]. 1 input Γ=(,ρc,(R,C),d,H,δ,ε) =( f, _c,(R,C),d,H,δ, ) ; // the problem input ε,δ∈(0,1] ,δ∈(0,1] ; // error and confidence thresholds input step∈(0,1]step∈(0,1] ; // step size scalar 2 3Ω∗← $ ^*_ γ$← Ω ; 4 πθ← $ _θ$← policy initialized with parameters θ∈ℝdpolicy initialized with parameters θ ^d; 5 (πθ∗,β∗)← $( _θ^*,β^*)$← SMC-ES(,ρc,(R,C),πθ,H,δ,ε) SMC-ES( f, _c,(R,C), _θ,H,δ, ) 6if (πθ∗,β∗)=⟂( _θ^*,β^*)= then return ⟂ ; 7 8while not all γi∈ are fixednot all γ_i∈ γ are fixed do 9 for each γi∈ that is not fixedeach γ_i∈ γ that is not fixed do old← $ γ_old$← γ ; // cache for rollback 10 11 γi← $γ_i$← γi+step×(γi,min−γi)γ_i+step×(γ_i, -γ_i); 12 13 ← $P_ γ$← diag(γ1λ1,…,γnλn)⊤Udiag(γ_1 _1,…,γ_n _n)U ; 14 15 Ω← $ _ γ$← ∈|⊤≤1 \ s \; |\; s P_ γ s≤ 1 \ 16 ρc′← $ _c $← ((Ω),)(U( _ γ),W); 17 (πθ,β)← $( _θ,β)$← SMC-ES(,ρc′,(R,C),πθ,H,δ,ε) SMC-ES( f, _c ,(R,C), _θ,H,δ, ); 18 19 if (πθ,β)=⟂( _θ,β)= then 20 ← $ γ$← old γ_old; 21 mark γi as fixedmark γ_i as fixed; 22 23 else if (πθ,β)≠⟂( _θ,β)≠ then 24 (Ω∗,πθ∗,β∗)← $( ^*_ γ, _θ^*,β^*)$← (Ω,πθ,β)( _ γ, _θ,β); 25 if γi≈γmin,iγ_i≈γ_ ,i then mark γi as fixedmark γ_i as fixed ; 26 return (Ω∗,πθ∗,β∗)( ^*_ γ, _θ^*,β^*) Algorithm 1 (ε,δ)( ,δ)-Lyapunov-guided Safe and Robust policy design problem Upon termination, the algorithm returns the tuple (Ω∗,πθ∗,β∗)( ^*_ γ, _θ^*,β^*), providing the final stability region Ω∗ ^*_ γ (and the induced scenario distribution ρc∗=((Ω∗),) _c^*=(U( ^*_ γ),W)), the optimized policy πθ∗ _θ^*, and a verified lower bound on the cumulative reward β∗β^*. By Proposizione 1, this solution comes with the following certificate: with confidence at least 1−δ1-δ, the probability of encountering a scenario (0,)∼ρc∗ ( s_0, w )\, \, _c^* such that πθ∗ _θ^* violates safety constraints or yields a cumulative reward below β∗β^* is at most ε . V Experiments We evaluate LyEvO through both simulation and real-world experiments. The simulation studies provide extensive safety and robustness assessment across a broad range of scenarios, while the real-world experiments examine the behavior of the learned policies and their sim-to-real transferability. V-A Implementation details V-A1 Case Studies We evaluate our approach on two classical nonlinear control systems. The first is cartpole, with a four-dimensional state and scalar action. The task is to track a commanded cart position while stabilizing the pole upright, i.e., , x=x^x= x, θ=0θ=0, with zero velocities. The second, more challenging benchmark is a high dimensional quadrotor goal-reaching problem with low-level thrust control: the state is twelve-dimensional, comprising position, attitude, and their linear and angular velocities, and the control input consists of the four individual rotor thrusts. The quadrotor must reach a commanded position [x^,y^,z^]⊤[ x, y, z] with all remaining state dimensions zero, corresponding to a stationary hover at the goal. For both systems, safety is enforced through state constraints: bounding cart position, pole angle, and their respective velocities for the cartpole, while restricting 3D position, translational velocities, Euler angles, and angular rates for the quadrotor. Both operate at 50Hz50Hz in simulation and hardware. Full setup details can be found in the supplementary code. V-A2 Baselines We compare our approach, LyEvO, and its robust version, LyEvO-R, which is trained by injecting zero-mean Gaussian noise into both observations (5%5\% multiplicative) and actions (1%1\% additive) [21], against the following baselines: i) Residual: a residual policy architecture that adds a learnable DRL correction to the fixed LMI-based policy solved as in sezione I-A, following [12]; i) SAC: a vanilla model-free DRL policy trained with soft actor-critic [30]; i) SAC-Lyapunov: SAC augmented with Lyapunov-based reward shaping, following [23]; iv) SAC-Lagrangian: SAC with constrained policy optimization via Lagrangian relaxation of the safety constraints [31]. All LyEvO experiments were performed on an HPC cluster. Each node provides two AMD EPYC 7301 CPUs (32 physical cores) and 256 GB of RAM, with hyper-threading disabled. Specifically, we leveraged OpenMPI [32] to parallelize the simulations during the SMC-ES() SMC-ES ( ) subroutine, using up to 1000 cores simultaneously. V-B Experiments and Results in Simulation We first evaluate all algorithms in simulation using the OpenAI Gym CartPole environment adapted from [33] and the PyBullet quadrotor environment adapted from [34]. We report two main metrics: i) Violation Probability (VP): probability of encountering an operational scenario where the policy fails to satisfy the safety constraints; i) Worst-case Return (WR): worst-case cumulative reward across evaluated scenarios. VP results are the output of SMC verification using ε,δ=1% ,δ=1\%. This means that with confidence at least 1−δ1-δ, the true VP is bounded by ε . For LyEvO, proposizione 1 unifies safety and performance verification. Thus, its reported WR is also a verified performance lower bound. As shown in tabelle I e I, LyEvO identifies approximated stability regions that are 6.14×6.14× and 224.04×224.04× larger than the standard certified regions for the Cartpole and 3D Quadrotor systems, respectively. Across both the standard and enlarged regions, LyEvO and it robust version LyEvO-R always satisfies safety constraints, demonstrating strong safety assurance and robust performance. The other DRL -based methods fail to pass formal verification. This is not unexpected, as these methods primarily focus on task performance while incorporating safety through soft penalties or auxiliary constraints. The resulting safety signal may therefore be insufficient to drive the policy toward uniformly safe behavior. Moreover, DRL policies can overfit to frequently encountered successful trajectories and fail to generalize to unseen conditions, which is exposed by our verification protocol. TABLE I: Safety and performance comparison in Cartpole simulation on the standard and enlarged stability regions. Standard Enlarged (6.14×6.14×) Alg. VP WR VP WR LyEvO 0 % ✓ 452.55452.55 0% ✓ 447.84447.84 LyEvO-R 0 % ✓ 445.61445.61 0% ✓ 445.24445.24 Residual 4.974.97% ✗ 11.2611.26 8.358.35% ✗ 9.539.53 SAC 13.6613.66% ✗ 7.627.62 20.2020.20% ✗ 1.301.30 Lyapunov 2.572.57% ✗ 11.4711.47 7.207.20% ✗ 9.629.62 Lagrangian 2.552.55% ✗ 10.2110.21 7.067.06% ✗ 7.787.78 TABLE I: Safety and performance comparison in Quadrotor simulation on the standard and enlarged stability regions. Standard Enlarged (224.04×224.04×) Alg. VP WR VP WR LyEvO 0% ✓ 447.90447.90 0% ✓ 459.86459.86 LyEvO-R 0% ✓ 477.20477.20 0% ✓ 469.05469.05 Residual 14.6014.60% ✗ 36.0436.04 40.6540.65% ✗ 9.159.15 SAC 8.588.58% ✗ 285.01285.01 18.6918.69% ✗ 124.73124.73 Lyapunov 5.265.26% ✗ 14.8614.86 14.9514.95% ✗ 19.8319.83 Lagrangian 47.6247.62% ✗ 128.05128.05 54.0554.05% ✗ 5.505.50 V-C Experiments Results in Real World (a) Cartpole (b) Quadrotor Figure 2: Real-world experimental platforms. (a) Cartpole testbed: linear rail with belt-driven cart and rigid pendulum. (b) Quadrotor flight arena equipped with a motion-capture system for state estimation TABLE I: Real-world Cartpole (no noise) across initial cart displacements |x0|∈0.1,0.2,0.28|x_0|∈\0.1,0.2,0.28\ m, target x=0x=0. Scenario Alg. Return Settle Time Pos Err Angle Err |x0|=0.10|x_0|=0.10 m LMI 969.70 953 0.010 ± 0.007 0.009 ± 0.006 LyEvO 985.61 770 0.008 ± 0.004 0.005 ± 0.003 LyEvO-R 996.36 58 0.004 ± 0.002 0.003 ± 0.002 |x0|=0.20|x_0|=0.20 m LMI 964.88 1000 0.023 ± 0.013 0.011 ± 0.007 LyEvO 985.53 699 0.008 ± 0.003 0.004 ± 0.003 LyEvO-R 991.12 72 0.005 ± 0.004 0.007 ± 0.005 |x0|=0.28|x_0|=0.28 m LMI 964.05 967 0.008 ± 0.005 0.007 ± 0.005 LyEvO 980.61 941 0.008 ± 0.006 0.007 ± 0.005 LyEvO-R 986.76 85 0.003 ± 0.001 0.002 ± 0.002 TABLE IV: Real-world Cartpole (with noise) across initial cart displacements |x0|∈0.1,0.2,0.28|x_0|∈\0.1,0.2,0.28\ m, target x=0x=0. Scenario Alg. Return Settle Time Pos Err Angle Err |x0|=0.10|x_0|=0.10 m LMI 964.45 922 0.043 ± 0.007 0.021 ± 0.008 LyEvO 988.12 910 0.028 ± 0.015 0.023 ± 0.014 LyEvO-R 994.75 72 0.031 ± 0.005 0.023 ± 0.006 |x0|=0.20|x_0|=0.20 m LMI 963.53 969 0.045 ± 0.005 0.020 ± 0.007 LyEvO 987.23 948 0.030 ± 0.016 0.024 ± 0.017 LyEvO-R 989.59 86 0.027 ± 0.004 0.021 ± 0.005 |x0|=0.28|x_0|=0.28 m LMI 963.60 118 0.012 ± 0.007 0.008 ± 0.005 LyEvO 979.86 1000 0.028 ± 0.015 0.023 ± 0.015 LyEvO-R 990.30 62 0.003 ± 0.002 0.003 ± 0.002 Figure 3: Trajectory comparison for different policies on Cartpole system in real world under noise. Figure 4: Gazebo Quadrotor experiments. The plot shows the tracking trajectories and lap time with mean tracking error. Figure 5: Real-world Quadrotor experiments under nominal conditions. From left to right: tracking trajectories, waypoint-wise tracking errors, and lap time with mean tracking error. Figure 6: Real-world Quadrotor experiments under disturbances created by a big power fan. In the real-world experiments, we exclusively compare formally verified policies, namely LyEvO and its robust variant LyEvO-R, against the mathematically certified LMI controller. These evaluations are conducted on physical Cartpole (Quanser) and Quadrotor (ANT-X) platforms. Performance is assessed using completion time and tracking error across different tasks. The experimental platforms are shown in Fig. 2(a) and Fig. 2(b). All three policies are tested under both nominal conditions and external disturbances generated by a high-power fan. V-C1 CartPole We evaluate recovery from different initial cart positions under both nominal and disturbed conditions. Each experimental trajectory is executed for H=1000H=1000 steps. As shown in tabelle I e IV, LyEvO-R achieves the highest returns and generally the shortest settling times across all tested initial conditions. Under nominal conditions, the settling time tends to increase with the initial displacement, reflecting the greater recovery effort required from states farther from equilibrium. Under disturbances, this trend becomes less consistent because the unmodeled, time-varying forces affect the transient response differently across trials. The trajectories in Fig. 3 provide a more detailed comparison for the disturbed case with x=0.28x=0.28. LyEvO-R approaches the equilibrium rapidly while exhibiting fewer oscillations and smaller transient deviations, resulting in the most stable overall response among the evaluated policies. V-C2 Quadrotor In this experiment, we evaluate policy in a 4×4×2.5m4× 4× 2.5\,m indoor flight cage using sequential waypoint tracking task under nominal and disturbed conditions, with setpoint changes triggered upon waypoint arrival. Before deployment on the physical platform, we conduct a cross-domain evaluation in a high-fidelity Gazebo simulator [35]. Each policy is evaluated over three consecutive runs to assess the consistency of its performance. As shown in Fig. 4, the three certified policies achieve comparable results in this setting. We then deploy them on the real quadrotor to evaluate their behavior under real-world model mismatch and disturbances. As shown in Fig. 5 and Fig. 6, LyEvO-R achieves the smoothest trajectories and the lowest average tracking error under both nominal and disturbed conditions, while retaining competitive task-completion times. LyEvO completes the maneuver more quickly, but its more aggressive response leads to larger tracking errors and less stable transients. These results suggest that training with observation and action noise encourages LyEvO-R to adopt a smoother and more conservative control strategy that is less sensitive to perturbations. The LMI controller, by contrast, requires longer completion times and exhibits limited robustness in the real-world experiments. The target reversals can drive the quadrotor beyond its certified safe region, where its nominal stability guarantees no longer apply. Combined with model mismatch and external disturbances, this limitation ultimately leads to failure under the disturbed condition. VI Discussion and Limitations This section highlights several practical considerations for real-world deployment. First, in policy optimization, ES is typically less sample-efficient than DRL [36]. Specifically, when using up to 1000 cores, LyEvO required 2.46 h for the nominal Cartpole (1.53 h for LyEvO-R) and 14.33 h for the Quadrotor (31.54 h for LyEvO-R). In contrast, training the DRL baselines for 1M steps required approximately 4 hours for Cartpole and 10 hours for the quadrotor on a single CPU core (AMD 9950X × 32). Second, the efficiency of the expansion procedure depends on the step size: large steps may discard feasible expansion directions, whereas small steps increase the number of iterations. In practice, the step size should therefore balance expansion speed and optimization robustness. Finally, the learned policy exhibits more actuation jitter than the certified LMI controller. Incorporating smoothness constraints or structure-preserving action parameterizations could reduce high-frequency variations and improve hardware robustness. VII Conclusion This paper presents LyEvO, a Lyapunov-grounded framework for safe and robust sim-to-real control. LyEvO unifies constrained Evolutionary Optimization, Statistical Model Checking (SMC) -based verification and Lyapunov-based stability region expansion. By exploiting prior system knowledge, it focuses training and evaluation on safety-relevant conditions and provides statistical evidence of deployment readiness beyond nominal performance. Experiments on Cartpole and 3D Quadrotor benchmarks, including real-world deployment, demonstrate its practical value. Future work will target more complex systems, more efficient region expansion and policy search, and tighter links between statistical verification and mathematical guarantees. Lastly, while our current framework relies on a nominal linear system to initialize the candidate stability region (e.g., via LMI ), future work will explore extending this approach to general non-linear dynamics without requiring a prior linearized model. References [1] J. Hwangbo, I. Sa, R. Siegwart, and M. Hutter, “Control of a quadrotor with reinforcement learning,” IEEE Robotics and Automation Letters, vol. 2, no. 4, p. 2096–2103, 2017. [2] J. Garcıa and F. Fernández, “A comprehensive survey on safe reinforcement learning,” Journal of Machine Learning Research, 2015. [3] S. Gu, L. Yang, Y. Du, G. Chen, F. Walter, J. Wang, and A. Knoll, “A review of safe reinforcement learning: Methods, theories and applications,” IEEE Transactions on Pattern Analysis and Machine Intelligence, 2024. [4] H. Zhang, H. Chen, C. Xiao, B. Li, M. Liu, D. Boning, and C.-J. Hsieh, “Robust deep reinforcement learning against adversarial perturbations on state observations,” Advances in neural information processing systems, vol. 33, p. 21 024–21 037, 2020. [5] J. Tobin, R. Fong, A. Ray, J. Schneider, W. Zaremba, and P. Abbeel, “Domain randomization for transferring deep neural networks from simulation to the real world,” in 2017 IEEE/RSJ international conference on intelligent robots and systems (IROS). IEEE, 2017, p. 23–30. [6] M. Landers and A. Doryab, “Deep reinforcement learning verification: a survey,” ACM Computing Surveys, vol. 55, no. 14s, p. 1–31, 2023. [7] T. Dreossi, A. Donzé, and S. A. Seshia, “Compositional Falsification of Cyber-Physical Systems with Machine Learning Components,” Journal of Automated Reasoning, vol. 63, no. 4, p. 1031–1053, Dec. 2019. [8] K.-C. Hsu, H. Hu, and J. F. Fisac, “The Safety Filter: A Unified View of Safety-Critical Control in Autonomous Systems,” Annual Review of Control, Robotics, and Autonomous Systems, vol. 7, Jul. 2024. [9] J. Achiam, D. Held, A. Tamar, and P. Abbeel, “constrained evolutionary optimization,” in International conference on machine learning. PMLR, 2017, p. 22–31. [10] T. J. Perkins and A. G. Barto, “Lyapunov design for safe reinforcement learning,” Journal of Machine Learning Research, vol. 3, no. Dec, p. 803–832–803–832, 2002. [11] H. Cao, Y. Mao, L. Sha, and M. Caccamo, “Physics-regulated deep reinforcement learning: Invariant embeddings,” in International Conference on Learning Representations, vol. 2024, 2024, p. 3712–3756. [12] T. Johannink, S. Bahl, A. Nair, J. Luo, A. Kumar, M. Loskyll, J. A. Ojea, E. Solowjow, and S. Levine, “Residual reinforcement learning for robot control,” in 2019 International Conference on Robotics and Automation (ICRA). IEEE, 2019, p. 6023–6029. [13] R. Cheng, A. Verma, G. Orosz, S. Chaudhuri, Y. Yue, and J. Burdick, “Control regularization for reduced variance reinforcement learning,” in International Conference on Machine Learning. PMLR, 2019. [14] A. Patterson, S. Neumann, M. White, and A. White, “Empirical design in reinforcement learning,” Journal of Machine Learning Research, vol. 25, no. 318, p. 1–63, 2024. [15] B. Mehta, M. Diaz, F. Golemo, C. J. Pal, and L. Paull, “Active domain randomization,” in Conference on Robot Learning. PMLR, 2020, p. 1162–1176. [16] T. Eimer, A. Biedenkapp, F. Hutter, and M. Lindauer, “Self-paced context evaluation for contextual reinforcement learning,” in International Conference on Machine Learning. PMLR, 2021, p. 2948–2958. [17] Y. Liang, Y. Sun, R. Zheng, and F. Huang, “Efficient Adversarial Training without Attacking: Worst-Case-Aware Robust Reinforcement Learning,” in Advances in Neural Information Processing Systems, S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh, Eds., vol. 35. Curran Associates, Inc., 2022, p. 22 547–22 561. [18] H.-D. Tran, X. Yang, D. Manzanas Lopez, P. Musau, L. V. Nguyen, W. Xiang, S. Bak, and T. T. Johnson, “Nnv: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems,” in International conference on computer aided verification. Springer, 2020, p. 3–17. [19] A. Corso, R. Moss, M. Koren, R. Lee, and M. Kochenderfer, “A survey of algorithms for black-box safety validation of cyber-physical systems,” Journal of Artificial Intelligence Research, vol. 72, p. 377–428, 2021. [20] G. Agha and K. Palmskog, “A survey of statistical model checking,” ACM Transactions on Modeling and Computer Simulation (TOMACS), vol. 28, no. 1, p. 1–39, 2018. [21] R. Curcio, T. Mancini, and E. Tronci, “Smc-es: Automated synthesis of formally verified control policies,” arXiv preprint arXiv:2607.15003, 2026. [22] R. S. Sutton, D. McAllester, S. Singh, and Y. Mansour, “Policy gradient methods for reinforcement learning with function approximation,” Advances in neural information processing systems, vol. 12, 1999. [23] T. Westenbroek, F. Castaneda, A. Agrawal, S. Sastry, and K. Sreenath, “Lyapunov design for robust and efficient robotic reinforcement learning,” in 6th Annual Conference on Robot Learning. [24] I. Rechenberg, “Evolutionsstrategie,” Optimierung technischer systeme nach prinzipien derbiologischen evolution, 1973. [25] T. Salimans, J. Ho, X. Chen, S. Sidor, and I. Sutskever, “Evolution strategies as a scalable alternative to reinforcement learning,” arXiv preprint arXiv:1703.03864, 2017. [26] A. Atamna, A. Auger, and N. Hansen, “Linearly convergent evolution strategies via augmented lagrangian constraint handling,” in Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms, 2017, p. 149–161. [27] R. Kalman and J. Bertram, “Control system analysis and design via the second method of lyapunov: (i) continuous-time systems (i) discrete time systems,” IRE Transactions on Automatic Control, vol. 4, no. 3, p. 112–112, 1959. [28] F. Blanchini, “Set invariance in control,” Automatica, 1999. [29] S. P. Boyd and L. Vandenberghe, Convex optimization. Cambridge university press, 2004. [30] T. Haarnoja, A. Zhou, P. Abbeel, and S. Levine, “Soft actor-critic: Off-policy deep reinforcement learning with a stochastic actor,” in International Conference on Machine Learning (ICML), 2018. [31] S. Ha, P. Xu, Z. Tan, S. Levine, and J. Tan, “Learning to walk in the real world with minimal human effort,” in Proceedings of the 2020 Conference on Robot Learning, ser. Proceedings of Machine Learning Research, J. Kober, F. Ramos, and C. Tomlin, Eds., vol. 155. PMLR, 16–18 Nov 2021, p. 1110–1120. [32] E. Gabriel, G. E. Fagg, G. Bosilca, T. Angskun, J. J. Dongarra, J. M. Squyres, V. Sahay, P. Kambadur, B. Barrett, A. Lumsdaine et al., “Open mpi: Goals, concept, and design of a next generation mpi implementation,” in European Parallel Virtual Machine/Message Passing Interface Users’ Group Meeting. Springer, 2004, p. 97–104. [33] G. Brockman, V. Cheung, L. Pettersson, J. Schneider, J. Schulman, J. Tang, and W. Zaremba, “Openai gym,” 2016. [34] Z. Yuan, A. W. Hall, S. Zhou, L. Brunke, M. Greeff, J. Panerati, and A. P. Schoellig, “Safe-control-gym: A unified benchmark suite for safe learning-based control and reinforcement learning in robotics,” IEEE Robotics and Automation Letters, 2022. [35] N. Koenig and A. Howard, “Design and use paradigms for gazebo, an open-source multi-robot simulator,” in 2004 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) (IEEE Cat. No.04CH37566), vol. 3, 2004, p. 2149–2154 vol.3. [36] A. Y. Majid, S. Saaybi, V. Francois-Lavet, R. V. Prasad, and C. Verhoeven, “Deep reinforcement learning versus evolution strategies: A comparative survey,” IEEE transactions on neural networks and learning systems, vol. 35, no. 9, p. 11 939–11 957, 2023.