Formal Methods in AI (FMAI) is Dr. Francesco Belardinelli's research group at Imperial College London dedicated to mathematically grounded techniques for specifying, verifying, and monitoring intelligent systems deployed in safety-critical settings.
Methods that combine formal verification, synthesis, and neurosymbolic methods with modern ML and RL models, focusing on robustness, correctness, and alignment with high-level specifications.
Specification languages, causal reasoning, temporal and probabilistic logics, and synthesis tools for capturing what it means for AI systems to be safe, predictable, and auditable.
Reusable software components, benchmarks, and verification pipelines to make rigorous safety techniques practical for real-world deployments.
Featured library
Explore our main open-source library for building and evaluating safe reinforcement learning systems for both single and multi-agent systems with formal methods at the core.
Latest news
A quick snapshot of announcements, papers, and milestones from FMAI.
Our lab presented two papers at the 40th Annual AAAI Conference on Artificial Intelligence (AAAI-26) in Singapore, covering the topics of enhancing Reinforcement Learning performance via variance reduction through training a behaviour policy, and synthesisi...
Read moreWe collaborate across formal methods, programming languages, control, and machine learning to tackle questions such as:
The group works with academic and industrial partners on open-source tools, benchmarks, and case studies in robotics, cyber-physical systems, and foundation models.
For collaborations or student opportunities, please get in touch via e-mail: francesco[dot]belardinelli[at]imperial.ac.uk.