Vincent Trélat
Ph.D. student
I am a third-year Ph.D. student at Inria, in Nancy, France. My main research interests are logic, formal methods, (mainly interactive) theorem proving, set theory and automated reasoning. I make Lean proofs for a living.
I have been developing BEer, an encoder for B proof obligations in SMT-LIB 2.7 using higher-order logic.
Contact MePinned Projects
Selected GitHub repositoriesAbout Me
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 formal computer science at the very end of my master's degree.
From 2023 to 2026, 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
Selected papers, preprints, and formalizationsBARReL: A modern backend for Atelier B in Lean
Preprint, 2026Safely Encoding B Proof Obligations in SMT-LIB
(🏆 Best Paper Award) ABZ, 2025Substitutions for λ-free higher-order terms
Archive of Formal Proofs, 2024Correctness of a Set-based Algorithm for Computing Strongly Connected Components of a Graph
Archive of Formal Proofs, 2022Invited talks
Selected presentationsFrom Sets to Types: using the B Method with modern proof tools
UFMG, Belo Horizonte, Brazil, 5 Feb 2026Brewing the Soundness of BEer
IFM 2025, Paris, France, 2025Journée du GT LVP du GdR GPL
Paris, France, 2025EuroProofNet: Workshop on Automated Reasoning and Proof Logging
Paris, France, 2025BLaSST Meeting
Clearsy, Paris, France, 2025ABZ: Safely Encoding B Proof Obligations in SMT-LIB
Düsseldorf, Germany, 2025ICSPA Meeting
Paris, France, 2025Journée du GT LVP du GdR GPL
Paris, France, 2024VINO
Campo Tures, Italy, 2024VeriDis Retreat
Liège, Belgium, 2024AFADL: Enhancing B Language Reasoners with SMT Techniques
Strasbourg, France, 2024BLaSST Meeting
Clearsy, Paris, France, 2024Qualification
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
Ph.D. at INRIA
Loria, Nancy, France
2023 - today
Technical University of Munich
Research Intern at the Chair for Logic and Verification, Munich, Germany
2022 - 2023
Clearsy
R&D Engineer, Aix-en-Provence, France
2023