Our research develops mathematical and computational methods for verifying machine-learning models, autonomous AI agents and neuro-symbolic systems. The work spans foundational specification and model-checking questions, scalable verification algorithms, research software and increasingly complex learning-enabled systems. Alongside foundational work, we have applied these methods to real autonomous and perception systems in marine, automotive and aerospace settings.
For the research group, people and group activities, visit the Safe AI Lab.
Our research on the verification of machine learning models began in 2015 with methods for reachability analysis of neural networks and neural agent-environment systems. Since then we have developed optimisation-based verification, dependency analysis, symbolic bound propagation, adaptive refinement and splitting methods, with a recurring focus on improving scalability while retaining formal guarantees.
A second major theme is robustness: analysing model behaviour over sets of possible inputs rather than individual examples, including perturbations with geometric or application-level interpretations. This work has progressively extended verification from neural classifiers to richer perception models and tasks.
Recent results address geometric robustness at the scale of large image and video models, formal robustness verification for object localisation, and region-level robustness validation for vision-language and vision-language-action models over continuous photometric and geometric perturbations. The latest work scales this analysis to models with up to 32B parameters. Current research continues towards verification questions connecting multimodal perception with action.
Early optimisation-based reachability analysis for ReLU networks.
Extends neural reachability analysis to a learned agent interacting with an environment.
Uses dependencies between activations to strengthen and accelerate verification.
Introduces indirect-effect-guided splitting and a more efficient encoding of splitting constraints.
Scalable geometric robustness validation for image and video models, with formal soundness under the conditions stated in the paper.
Formal robustness bounds for object localisation in the paper’s stated detector setting.
Deep robustness validation study for SoA VLMs and VLAs against photometric/geometric perturbations scaling to 32B parameters.
Our research on the verification of autonomous agent systems began in 2000 by defining and exploring their model-checking problem: how to establish formally properties of individual and collective behaviour as agents interact. The specification formalisms include temporal, epistemic and strategic modalities, providing a rich framework for expressing how knowledge, capabilities and behaviour evolve over time.
This led to complementary bounded-model-checking and symbolic model-checking techniques, followed by increasingly sophisticated symbolic algorithms implemented in MCMAS and, subsequently, parameterised verification techniques for systems whose number of agents is not fixed in advance, including methods for verifying emergent behaviour in swarms.
More recently, we have extended these ideas to autonomous agents with learned components, including neural agent-environment systems in non-deterministic settings and agents with memory. Current work focuses on multimodal AI agents and on verification and validation questions arising when AI systems perceive and act in physical environments.
With Wojciech Penczek. SAT-based bounded model checking of temporal-epistemic properties over interpreted systems.
Model checking specifications combining knowledge and strategic ability.
Symbolic OBDD-based model checking for multi-agent systems.
Verification of collective behaviour in systems with varying numbers of agents.
Verification of families of systems independently of a fixed population size.
Branching-time verification of closed-loop neural agent-environment systems.
Temporal verification of neural agents with memory in uncertain and partially observable environments.
Our research on neuro-symbolic systems studies how to verify systems that combine learned components with symbolic or probabilistic reasoning. The verification target is the composed system: how uncertainty or perturbations affecting learned components propagate through reasoning and affect properties of the resulting system.
Earlier work investigated the strategic abilities of neural-symbolic multi-agent systems. Our NeSy 2025 Outstanding Paper Award work developed scalable probabilistic robustness verification, propagating input uncertainty through learned perception and symbolic reasoning. The forthcoming NeurIPS 2026 work extends this line to end-to-end verification of temporal neuro-symbolic systems, certifying trajectory-level decisions across learned perception and symbolic automata.
Formal verification of fault tolerance, self-diagnosability and recovery for Autosub6000, an autonomous underwater vehicle used for deep-ocean exploration. The work used an engineering Simulink/Stateflow model, automatic fault injection and MCMAS to analyse operation under degraded conditions.
Verification methods were evaluated on automotive perception models in collaboration with Audi, including a VGG16-based component of a multi-view 3D detector.
Work with Boeing Research & Technology applied neural-network verification to aircraft-domain systems, including open-category detection, landing-assistance/collision-avoidance settings, and semantic key-point detection for aircraft pose estimation/autoland.
MCMAS is an open-source symbolic model checker for multi-agent systems. It enables the verification of multi-agent systems, expressed in the Interpreted Systems Programming Language (ISPL), against temporal, epistemic and strategic specifications. Its algorithms use ordered binary decision diagrams to represent and analyse state spaces, with support for fairness, counterexamples and witness executions. The STTT journal article provides the main account of its semantics, verification algorithms and implementation.
Venus is a neural-network verification tool for reachability and robustness properties of ReLU-based networks. It combines mixed-integer optimisation with dependency analysis, bound propagation and splitting methods developed in our work. The tool was one of the software outputs of the DARPA Assured Autonomy effort.
VeriNet is a neural-network verification tool based on variants of symbolic interval propagation developed in our work, combined with adaptive refinement and adversarial search. A feature of the approach is its iterative bound tightening and support for networks with several activation functions.
Principal Investigator
Research on verification methods for establishing guarantees about autonomous and robotic systems incorporating machine learning.
Founding co-director
Joint programme with King’s College London.
Principal Investigator
EU Horizon-funded research on robust learning and reasoning for complex-event forecasting, including formal verification of systems combining learning and symbolic reasoning.
Principal Investigator
Research on mathematical methods and tools for verification of machine-learning systems.