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. Read more...

Mathematical modeling of microalgal growth – hybrid and data-driven approaches for multi-scale prediction

Nov 23 14:00 ₂₀₂₆

Monday, 23 November, 2pm
Amphi Dorothy Hodgkin, ENS Paris-Saclay, Gif-sur-Yvette and online

Abstract: Microalgae have numerous applications, ranging from wastewater treatment to the production of proteins and biofuels. Developing these applications requires a better understanding and prediction of microalgal growth, particularly when moving from laboratory cultures to larger-scale systems. Read more...

Nov 3 14:00 ₂₀₂₆

Abstract: Cryptographic proofs proceed in large part by reductions to cryptographic assumptions expressed as games. These reductions rely on simulators which are often tedious to write and involve a significant amount of trivial code. Thus, simulators are only sketched in pen-and-paper proofs, which is error-prone. Mechanized cryptographic proofs remove the risk of errors, but requiring users to explicitly write simulators is an unreasonable burden. In this paper, we consider the problem of simulator synthesis in Squirrel, where cryptographic simulation is expressed as bi-deduction. Although the seminal work on bi-deduction provides a proof system and a simple proof-search procedure for it, we show that it suffers from systematic failures when working with games such as IND-CCA2. We provide a significantly improved procedure, that can re-use oracle calls across recursive iterations, and generates precise invariants to justify it. We implement this procedure in Squirrel and validate it in a proof of ballot privacy for the FOO e-voting protocol, which is the first computational mechanized proof for FOO, and the most complex Squirrel proof to date.

Formal methods for psychology and consciousness science

Nov 30 9:00 ₂₀₂₆

Monday, November 30st, 9am
Room 1B26, ENS Paris-Saclay, Gif-sur-Yvette

Abstract: Psychological and neurocognitive theories are frequently stated in natural language. Such verbal theories often contain ambiguities and leave key components underspecified, which makes them difficult to validate or falsify. This thesis introduces a framework to formally build and analyze some parts of psychological and neurocognitive theories, drawing on formal methods from theoretical computer science: communicating, timed, and probabilistic automata, refinement, and model checking. 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...

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...