Création d'outils interactifs pour le développement de preuves formelles en Rocq, et interfaçage avec des LLMs

Contexte et atouts du poste

Rocq est logiciel, appelé prouveur interactif, conçus pour écrire et valider des preuves de propriétés mathématiques grâce à une interaction entre utilisateurices et machine. Par exemple, ils sont utilisés dans le monde académique ainsi que dans l’industrie pour prouver la correction de programmes critiques et sophistiqués dans des domaines variés (cybersécurité, compilation, architecture, etc.). L’une des forces de ce type de méthodes formelles est son expressivité, qui permet en fait de formaliser et de vérifier des théories mathématiques arbitrairement sophistiquées. De fait, ces prouveurs interactifs sont aussi utilisés par des chercheurs en mathématiques aussi bien que par des chercheurs en méthodes formelles.

Un des grands défi de ce domaine est de démocratiser la production des bibliothèques de code de ces prouveurs, et de leur concevoir un environnement de développement moderne et productif. Le contexte général de ce...