Alessio Coltellacci (Veridis), défendra sa thèse intitulée

Reconstruction des preuves SMT dans Lambdapi.

La soutenance se déroulera en anglais le lundi 26 janvier 2026 à 14h au LORIA, en salle C005. Elle sera suivie d’un pot devant la salle.

Pour ceux qui ne pourraient pas venir, la soutenance sera diffusée en visio (accessible à partir de 14h00, possibilité de rejoindre depuis un navigateur web) :

https://cnrs.zoom.us/j/95435518789?pwd=RiIzDeE5HIJEofM1x4g3raM9KZ3Y5x.1

Jury :

• Laura Kovács, Vienna University of Technology (rapporteuse)
• Alexander Steen, University of Greifswald (rapporteur)
• Chantal Keller, LMF/Université Paris-Saclay (examinatrice)
• Mathias Fleury, University of Freiburg (examinateur)
• Régine Laleau, Université de Paris-Est Créteil (examinatrice)
• Stephan Merz, INRIA/Université de Lorraine (directeur de thèse)

Résumé :

Les démonstrateurs automatiques de théorèmes modernes sont de plus en plus plébiscités pour établir la correction de systèmes informatiques critiques. Parmi eux, les solveurs de satisfiabilité modulo des théories (SMT) occupent une place centrale, en raison de leur grande expressivité et de leur efficacité dans le traitement de raisonnements logiques complexes. Cependant, l’ampleur de leur base de code, conjuguée à la sophistication de leur architecture logicielle, rend toute vérification formelle exhaustive impraticable, soulevant ainsi une question fondamentale de confiance:

Dans quelle mesure peut-on accorder foi à la correction des résultats produits par ces solveurs ?

Une réponse particulièrement prometteuse à cette problématique réside dans le recours à la journalisation de preuves (proof logging), approche consistant à faire produire par les solveurs des traces de preuve susceptibles d’être vérifiées de manière indépendante par des vérificateurs externes. Le format Alethe est récemment apparu comme un standard pour représenter de telles preuves SMT. Plusieurs solveurs SMT ont adopté le format Alethe. Néanmoins, l’absence actuelle d’un vérificateur de preuves certifié pour Alethe en limite encore l’adoption.

Dans cette thèse, nous proposons un outil permettant de traduire les preuves SMT produites au format Alethe vers l’assistant de preuve Lambdapi, une implémentation du λΠ-calcul modulo la réécriture. Lambdapi est un assistant de preuve fondationnel, basé sur la théorie des types dépendants et sur des règles de réécriture, conçu pour servir de pivot pour l’échange de preuves entre assistants de preuve interactifs. Nous présentons un encodage modulaire de la logique SMT et des règles Alethe dans Lambdapi, couvrant des théories fondamentales telles que le raisonnement du premier ordre et l’arithmétique linéaire.

Nous détaillons ensuite le processus de reconstruction, qui requiert des techniques telles que la démonstration par réflexion et l’élaboration de simplifications spécifiques aux solveurs. Enfin, nous évaluons notre implémentation sur des benchmarks et montrons que les preuves Alethe générées par des solveurs SMT modernes peuvent être reconstruites de manière efficace et fiable dans Lambdapi, ouvrant ainsi la voie à des preuves SMT à la fois vérifiées et portables.

Alessio Coltellacci (Veridis), will defend his thesis entitled

Reconstructing SMT Proofs in Lambdapi.

The defense will be held in English on Monday 26th, 2026 at 2:00 P.M. at LORIA, in room C005.
The defense will be followed by a pot de thèse in front of the room.

For those who cannot attend in person, the defense will be streamed online (accessible from 2 P.M., you can join directly from a web browser):

https://cnrs.zoom.us/j/95435518789?pwd=RiIzDeE5HIJEofM1x4g3raM9KZ3Y5x.1

Jury:

• Laura Kovács, Vienna University of Technology (reviewer)
• Alexander Steen, University of Greifswald (reviewer)
• Chantal Keller, LMF/University Paris-Saclay (examiner)
• Mathias Fleury, University of Freiburg (examiner)
• Régine Laleau, University Paris-Est Créteil (examiner)
• Stephan Merz, Inria/University of Lorraine (PhD supervisor)

Abstract:

Powerful modern automated theorem provers are increasingly used to establish the correctness of critical computer systems. Among them, Satisfiability Modulo Theories (SMT) solvers play a central role thanks to their expressive power and efficiency in handling complex logical reasoning tasks. However, their size and complexity make full formal verification of their implementations impractical, raising a fundamental question of trust:

Can we trust the correctness of their results?

A promising answer lies in proof logging, where solvers produce proof traces that proof checkers can independently check. The Alethe format has recently emerged as a unified framework for representing such SMT proofs. Several SMT solvers have adopted the Alethe format. However, Alethe lacks a certified proof checker, limiting its adoption and trustworthiness.

In this thesis, we propose a reconstruction framework that translates Alethe proof traces into the Lambdapi proof assistant, an implementation of the λΠ-calculus modulo rewriting. Lambdapi is a foundational proof assistant based on dependent type theory and rewriting rules, intended to serve as a pivot for exchanging proofs between interactive proof assistants. We present a modular encoding of SMT logic and Alethe rules in Lambdapi, covering core theories such as first-order reasoning and linear arithmetic.

We detail the reconstruction process, which requires techniques such as proof by reflection and the elaboration of solver specific simplifications. Finally, we evaluate our implementation on benchmark examples and demonstrate that Alethe proofs generated by modern SMT solvers can be efficiently and reliably reconstructed in Lambdapi, paving the way toward portable and independently verifiable SMT proofs.