  With the increasing system complexity and attack sophistication, the
necessity of autonomous cyber defense becomes vivid for cyber and
cyber-physical systems (CPSs). Many existing frameworks in the current
state-of-the-art either rely on static models with unrealistic assumptions, or
fail to satisfy the system safety and security requirements. In this paper, we
present a new hybrid autonomous agent architecture that aims to optimize and
verify defense policies of reinforcement learning (RL) by incorporating
constraints verification (using satisfiability modulo theory (SMT)) into the
agent's decision loop. The incorporation of SMT does not only ensure the
satisfiability of safety and security requirements, but also provides constant
feedback to steer the RL decision-making toward safe and effective actions.
This approach is critically needed for CPSs that exhibit high risk due to
safety or security violations. Our evaluation of the presented approach in a
simulated CPS environment shows that the agent learns the optimal policy fast
and defeats diversified attack strategies in 99\% cases.
