The Laboratoire Méthodes Formelles (LMF) was founded on 1 January 2021 as a joint research centre of University Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, and CentraleSupélec with a main focus on formal methods. The new laboratory combines the expertise of about 100 members from the former Laboratoire Spécification et Vérification (LSV) and the VALS team of Laboratoire de Recherche en Informatique (LRI).

In our mission to enlighten the digital world through Mathematical Logic, we rely on formal methods as a tool to analyse, model, and reason about computing systems, such as computer programs, security protocols, and hardware designs. Our research targets a wide range of computational paradigms, from classical to emerging ones such as biological and quantum computing.

LMF is structured around three hubs: Proofs and Models, which lie at the heart of our historical background, and Interactions, that is aimed at fostering cross-fertilisation between formal methods and other domains in computing science and beyond.

© Laurent Ardhuin pour le CNRS

Patricia Bouyer-Decitre (LMF, CNRS, ENS Paris-Saclay) has been awarded the CNRS Silver Medal 2026 in recognition of her contributions to formal methods, automata theory, logic, and game theory. This prestigious distinction honors researchers for the originality, quality, and impact of a body of work that significantly advances research at the national and international levels.

Read more...

Stéphane Demri, CNRS researcher at LMF, has published Concise Introduction to Alternating-Time Temporal Logics: A Guide for Understanding the Model-Checking Problem.

From the publisher’s description: ''This textbook provides a concise presentation of alternating-time temporal logics dedicated to strategic reasoning in multi-agent systems. Read more...

Oct 1 10:30 ₂₀₂₆

Abstract: Concurrent monads, due to Rivas and Jaskelioff, are a specialization of monads, namely a relaxation of lax monoidal monads (commutative monads) in ordered category theory. For the application in categorical semantics of functional programming languages, they are an abstraction of notions of effectful computation that are composable not only sequentially but also in parallel. Both the sequential and parallel compositions are unital and associative; more significantly, they are interrelated by interchange inequations. Concurrent monads categorify the ordered-algebraic concept of concurrent monoids from concurrency theory, going back to Grabowski and Gischer.

I will motivate and introduce this elegant abstraction, which treats parallel composition on a par with sequential composition, present some theory and show some examples from programming language semantics and concurrency theory.

Translations of Proofs between Higher-Order Logics and between Theories with Rewriting

Sep 24 14:00 ₂₀₂₆

Thursday, 24 September 2026 at 2pm
Amphi 1, Eiffel building, CentraleSupélec, Gif-sur-Yvette

Abstract: Formal proofs and proof assistants are rigorous tools for expressing theorems and verifying their validity. Formal proofs can be based on a wide variety of logics, implemented in various proof assistants, and use numerous data structures or representations. The goal of this thesis is to design translations of formal proofs between such formalisms.

Read more...

Quantum Cellular Automata and Quantum Field Theories

Sep 24 14:00 ₂₀₂₆

Thursday, 24 September 2026 at 2pm
Room 1B26, ENS Paris-Saclay, 4 Av. des Sciences, 91190 Gif-sur-Yvette

Abstract: This thesis studies Quantum Cellular Automata (QCAs) as discrete-spacetime, strictly local, and unitary models of quantum field theories, with a focus on lattice artifacts, their resolution, and the digital quantum simulation of gauge theories.

We extend the gauged-QCA framework to non-Abelian symmetries, building the first QCA model coupling (1+1)D Dirac fermions to an SU(2) Yang–Mills gauge field.

Read more...

The annual program verification competition VerifyThis took place in Turin, as part of ETAPS 2026. Among 24 participating teams, two teams from LMF received prizes, including the main award:

• Best Overall Team: Li-yao Xia and Jacques-Henri Jourdan
• Best One-Person Team: Jean-Christophe Filliâtre

Read more...