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 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.
28 Jan 2026
Two papers presented at AAAI-26!
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 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.