This talk overviews research at Caltech on designing hybrid or neurosymbolic AI systems that blend learning with symbolic structure, in order to achieve both the flexibility of the former and the formal interpretability and generalization power of the latter.  By having systems that are formally interpretable, one can employ a wide range of formal analysis techniques to verify important properties of the overall system, such as those related to safety and stability, as well as use those analyses to guide system design and optimization.  Focusing on formally interpretable structure arising from control and planning, I will present new algorithms and their deployment in a range of applications, including agile flight control under challenging and time-varying environments, controlling highly underactuated systems (e.g., one-legged hoppers), as well as briefly overview other related research.