Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
- 15:00 7th May 2026 ( week 2, Trinity Term 2026 )Seminar Room 051
Formal verification of neuro-symbolic cyber-physical systems, such as drones, medical devices and robots, is complicated. Neural components must be trained to be optimal with respect to the available data as well as the safety specifications, and then verified using specialised solvers. Symbolic models of the “cyber” and “physical” behaviour of the system must be constructed and verified in interactive theorem provers (ITPs), often requiring mature mathematical libraries to reason about the interplay of discrete and continuous dynamics, preferably obtaining infinite time-horizon guarantees. Finally, the results of the two already challenging verification tasks need to be integrated into a single proof in a coherent and consistent way, whilst preserving deployability of the resulting model.
In this talk we present a compositional methodology for constructing such proofs. The Vehicle framework provides a functional, domain-specific language for specifying, training, and verifying neural components. We extend Vehicle to allow integration with any ITP with minimal effort, thereby bridging the gap between the neural and symbolic proofs. First, we describe how Vehicle’s standard bidirectional type checker can be reused to transpile neural specifications into an intermediate representation targeting multiple theorem provers. Second, we integrate Vehicle with Rocq, Isabelle/HOL, Agda and the industrial prover Imandra; and showcase a generic infinite time-horizon safety proof of a discrete cyber-physical system with a neural network controller in each ITP. Finally, to put the idea of compositional neural-cyber-physical system verification to the test, we use the Mathematical Components libraries in Rocq to verify infinite time-horizon safety of a medical device, modelled as a continuous cyber-physical system with a neural controller. To our knowledge, this is the first result of this kind in a general purpose ITP; and a result that was only feasible thanks to the compositionality provided by Vehicle’s functional interface.
Speaker bio
Ekaterina Komendantskaya is a professor at Heriot-Watt and Southampton universities. Her research is dedicated to neuro-symbolic methods; most recently — to applications of formal methods in verification of machine learning and of complex systems with machine learning components. She has published over 90 papers in international venues, including CAV, ESOP, ITP, AAAI, ICLP, PPDP; has given dozens of invited talks, including most recently at ICFP'25, FSCD'25, Edinburgh Center for Robotics, Newton Institute Cambridge, Dagstuhl. She has been in the PC of main Logic and Programming Language conferences (POPL, LICS, ITP, CAV, ESOP, ICFP, ICLP, FLOPS, PPDP, PADL), and has been serving as a PC chair of PPDP19, PADL'20, MPC'22, FLOPS'26, ITP'26. She has held individual and collaborative research grants to the total value of £ 16 million. Currently, she is an ``ARIA Creator" in the Mathematics for Safe AI project run by ARIA, the Advanced Research and Innovation Agency. She is a CoI and lead of Verification training in the CDT on Dependable and Deployable AI for Robotics, Edinburgh, UK.Alistair Sirman is a 1st year PhD student at the University of Southampton. His interests are in Formal Methods and interactive theorem proving, focussing on verification in machine learning and certificates. His PhD project is funded by the UKRI Industrial Partnership Scheme, and conducted in collaboration with the SLB Cambridge research lab. He organises weekly causal logic seminars for those interested to discuss their work and interests, is a lab tutor teaching Haskell and formal verification to undergraduates, and completed a dissertation on a potentially verifiably safe train scheduling algorithm. His interest in programming languages spans paradigms, where he created a game engine and editor from scratch using C++ and OpenGL, and working as a lone full-stack developer on comprehensive engineering software.