Le Laboratoire Méthodes Formelles (LMF) est né le 1er janvier 2021 de la volonté politique de ses tutelles - Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria et CentraleSupélec - de créer un pôle ciblé sur les méthodes formelles. Le LMF est formé du Laboratoire Spécification et Vérification (LSV, ENS Paris-Saclay, CNRS, Inria) et de l’équipe Vals du Laboratoire de Recherche en Informatique (LRI, Université Paris-Saclay, CNRS, Inria, CentraleSupélec) soit une centaine de personnes.

Son ambition est d’éclairer le « monde numérique » grâce à la logique mathématique en utilisant les méthodes formelles comme outil d’analyse, de modélisation et de raisonnement pour les programmes informatiques, les protocoles de sécurité, etc. Il s'appuie sur des paradigmes de calcul des plus classiques aux plus novateurs comme l’informatique quantique.

Le LMF est structuré en pôles : son cœur de métier en comporte deux, « Preuves » et « Modèles » ; le troisième, « Interactions », est une ouverture à d’autres domaines tels que l’IA et la biologie.

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

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

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.

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

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