The objective of the proposed research is to advance the use of Interval Markov Decision Processes (IMDP) for complex task planning on learning-enabled legged locomotion systems. IMDP methodologies show great promise for verification and synthesis of control policies for complex robotic tasks. In particular, IMDPs provide formal guarantees on robot behavior in the presence of system and environmental uncertainties. Learning techniques such as Gaussian processes (GP) will be used to formally quantify uncertainty, bridging the gap between low-level dynamical considerations and high-level planning. The ultimate aim is to develop a unified robotic planning framework which accommodates complex high-level tasks and enables novel locomotion behaviors while operating in highly uncertain environments.