Some of our latest work on Neurosymbolic AI, involving formal verification and neural networks, was presented at LogicNN (Logical Methods for Neural Network Analysis), FLOC 2026. The associated paper (IsaGrad: Verified Automatic Differentiation over Computational Graphs in Imperative HOL) on the work in progress is available here.