This project advances science at the intersection of robotics, artificial intelligence, and formal verification to enable reliable and transparent robot behavior in real-world settings. As robots increasingly assist with complex tasks—from warehouse logistics to supporting independent living—ensuring their safe and trustworthy operation is essential. However, state-of-the-art robot learning methods, such as deep reinforcement learning, rely heavily on opaque neural network controllers that are difficult to interpret, verify, and generalize, limiting their use in safety-critical domains. This research addresses these challenges by developing a new class of interpretable control programs, written in domain-specific languages with automatically-inferred domain knowledge. These programs enable robots to reason over long-term goals, adapt to novel environments, and be certified as safe before deployment. Through this approach, the project aims to improve both the efficiency and reliability of real-world robotic systems. The main contributions of this project are new algorithms for the synthesis and verification of robot-control programs, grounded in formal methods, to support transparent and trustworthy robot learning. The proposed approach synthesizes high-level symbolic programs from low-level reward functions or task specifications in continuous, high-dimensional environments. At its core is abstraction refinement, which automatically generates and iteratively improves symbo