Towards
Verifiable AI

Developing scalable verification methods and formal guarantees for machine learning models, autonomous AI agents and neuro-symbolic systems.

Explore our research

From formal logic to verifiable AI systems.

Research

Research directions

Verification of
Machine Learning Models

Methods for verifying and validating neural networks, including object detectors, vision transformers and multimodal models, with a focus on robustness and scalability.

Verification of
Autonomous AI Agents

Verification methods for agents in uncertain environments, including perception, memory, and learning, now extending to multimodal agents and physical AI.

Verification of
Neuro-symbolic Systems

Methods for verifying systems that combine learned components with symbolic and probabilistic reasoning, with an emphasis on end-to-end robustness guarantees.

Formal Guarantees
Scalability
Robustness
Real-world Applicability

Research themes over time

Selected themes and transitions in the research programme.

1990s–2000Formal logic for multi-agent systemsPhD in formal epistemic logic, 1999.
2000sModel checking multi-agent systemsScalable, automated verification.
2010–2017Scaling verificationParameterised systems, swarms and abstraction.
2015–2020Verification of machine learning modelsNeural models and robustness.
2020–2024Scalability and robustnessRicher perception models and modalities.
2025–Verification of multimodal and agentic AIVLMs, VLAs and physical AI.

Verification software

Software and documentation

MCMAS

Open-source model checking for multi-agent systems.

Venus

Verification of neural networks and machine learning models.

VeriNet

Scalable verification of neural networks.

Recent Selected Work

All publications

Original H²V Figure 1 crop showing Hilbert space-filling dimensionality reduction beside the corresponding Hölder optimisation construction.

Scalable Neural Network Geometric Robustness Validation via Hölder Optimisation

NeurIPS 2025

H²V validates geometric robustness in large image and video models, scaling to 300 million tunable parameters. A separate 2026 preprint extends the approach to VLMs and VLAs with up to 32 billion parameters.

Explore this work

Illustrative street scene with vehicles and detection boxes, representing object detection research; not a figure from the IoUCert paper.

IoUCert: Robustness Verification for Anchor-based Object Detectors

ECCV 2026

Formal robustness verification for anchor-based SSD and YOLO detector variants under brightness, contrast and motion-blur perturbations.

Explore this work

Public NeSy 2025 figure unavailable Neuro-symbolic verification illustration from the public NeSy 2025 paper, showing neural components and symbolic reasoning; not a figure from the forthcoming NeurIPS 2026 paper.