The widespread deployment of reinforcement learning (RL) systems in real-world applications necessitates rigorous guarantees of their correctness. In the RL system, an agent iteratively interacts with the environment, with the objective of maximizing cumulative rewards. These interactions involve constraints of states, actions, and rewards, where any violation of these constraints indicates a system-level error. In this paper, we propose an SMT-based framework for the formal modeling of RL systems. Our method encodes constraints for RL components as SMT formulas, and cumulative reward maximization as an optimization objective, enabling automated verification of constraint satisfiability through SMT solvers. We evaluate our formal modeling approach through experiments conducted on a popular RL environment. Experimental results validate the effectiveness of our method in identifying constraint violations and ensuring behavioral correctness.