Vincent Trélat
Ph.D. student · Inria Nancy · VeriDis
My main research interests are logic, formal methods, interactive theorem proving, set theory and automated reasoning. I make Lean proofs for a living.
News
Recent updates
- Nov 10, 2026 PhD defense at Inria Nancy. Upcoming
Pinned Projects
Selected GitHub repositories
About
My introduction
Despite my early beginnings in applied physics and mathematics, and my engineering degree from the École des Mines, I took a sharp turn toward formal computer science at the very end of my master's degree.
From 2023, I've been working as a PhD student at Inria Nancy. My work focuses on improving the automation of the B method and articulates techniques from set theory and automated reasoning. I mostly work with Lean, a fantastic programming language and theorem prover.
Apart from my studies, I like cycling, cooking, photography, playing guitar and capybaras.
Publications
Papers, preprints, and formalizations
BARReL: A Modern Backend for Atelier B in Lean
ZFLean: a framework for set-level mathematics in Lean
Brewing the Soundness of BEer
Safely Encoding B Proof Obligations in SMT-LIB 🏆 Best Paper
Amélioration des raisonneurs du langage B avec des techniques SMT
Substitutions for λ-free higher-order terms
Correctness of a Set-based Algorithm for Computing Strongly Connected Components of a Graph
Invited talks
Selected presentations
BARReL: a modern backend for Atelier B in Lean
AFADL 2026 — GdR SciLog, Lille, France, 2026
From Sets to Types: using the B Method with modern proof tools
UFMG, Belo Horizonte, Brazil, 2026
Brewing the Soundness of BEer
IFM 2025, Paris, France, 2025
Journée du GT LVP du GdR GPL
Paris, France, 2025
EuroProofNet: Workshop on Automated Reasoning and Proof Logging
Paris, France, 2025
BLaSST Meeting
Clearsy, Paris, France, 2025
ABZ: Safely Encoding B Proof Obligations in SMT-LIB
Düsseldorf, Germany, 2025
ICSPA Meeting
Paris, France, 2025
Journée du GT LVP du GdR GPL
Paris, France, 2024
VINO
Campo Tures, Italy, 2024
VeriDis Retreat
Liège, Belgium, 2024
AFADL: Enhancing B Language Reasoners with SMT Techniques
Strasbourg, France, 2024
BLaSST Meeting
Clearsy, Paris, France, 2024
Qualification
My personal journey
École Nationale Supérieure des Mines de Nancy
University of Lorraine, Nancy, France
2020–2023
Technical University of Munich
Munich, Germany
2022–2023
French Preparatory Classes for Higher Education
Orléans, France
2018–2020
Post-doc at MPI
MPI-SWS, Saarbrücken, Germany
2026–
Ph.D. at Inria
LORIA, Nancy, France
2023–2026
Technical University of Munich
Research Intern, Chair for Logic and Verification, Munich, Germany
2022–2023
Clearsy
R&D Engineer, Aix-en-Provence, France
2023
Cycling
Some of my cycling activities
Past students
Matteo Pouillat
Telecom Nancy, Université de Lorraine
Contact
Get in touch
Location
B206, INRIA Nancy Grand-Est, Loria, France