Integrating machine learning and control systems has achieved remarkable success in controlling complex dynamical systems such as autonomous vehicles. However, the resulting controlled system often has a neural network (NN) in the loop which represents the system dynamics, control policy, or perception. The nonlinearity and large scale of NNs make it challenging to provide formal safety or stability guarantees for such learning-enabled systems. This thesis focuses on developing specialized numerical tools for efficiently analyzing NN dynamical systems and a novel robust model predictive control (MPC) framework that is promising for controlling NN dynamical systems with safety guarantees. In the first part of the thesis, I demonstrate how to build a hierarchy of verification methods for isolated output range analysis of NNs, closed-loop reachability analysis, and closed-loop stability analysis of NN dynamical systems. In the second part, I present a novel robust MPC method for uncertain linear dynamical systems with significantly reduced conservatism compared with existing baselines and discuss the possibility of combining NN verification tools and robust MPC for safe control of complex dynamical systems.