21 Sept 2026
FMAI at EUMAS 2026: tutorial and paper accepted
Our Formal Methods for Safe Reinforcement Learning tutorial and a paper on contract-based compositional shielding are part of EUMAS 2026 in Malmö, Sweden.
Read moreFormal Methods in AI
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.
Affiliated with 
Research
Verification for RL Systems
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.
Methods
Specifications, Logics, and Synthesis
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.
Practice
Infrastructure and Open-Source Tooling
Reusable software components, benchmarks, and verification pipelines to make rigorous safety techniques practical for real-world deployments.
Featured library
MASA-Safe-RL
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.
Main Library
Repository
sacktock / MASA-Safe-RL
Latest news
Updates from the group
A quick snapshot of announcements, papers, and milestones from FMAI.
5 Jun 2026
Can You Train AI to Stay Safe? Meet us at the Great Exhibition Road Festival
Meet the FMAI lab at the Great Exhibition Road Festival and try our interactive safe AI demo.
Read more
11 Mar 2026
Tutorial accepted at AAMAS 2026: Formal Methods for Safe Reinforcement Learning
Our tutorial for AAMAS 2026 was accepted! The tutorial covers key techniques for Safe Reinforcement Learning and is intended for a broad audience.
Read moreWhat we focus on
We collaborate across formal methods, programming languages, control, and machine learning to tackle questions such as:
- Providing formal guarantees of permissive safety for single and multi-agent reinforcement learning agents.
- How to prove properties of models that learn and update over time.
- How to detect and mitigate violations at runtime with guarantees.
- How to integrate verification into existing RL, ML and engineering workflows.
Collaborations & community
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.