Collaborations & partenariats
Le CFVL est ouvert aux collaborations académiques avec les laboratoires en méthodes formelles, sécurité systèmes, compilation vérifiée et cryptographie formelle.
Recherche collaborative
La vérification formelle est un domaine exigeant qui requiert une interaction étroite entre recherche académique et application industrielle. Le CFVL s’inscrit dans cette logique de collaboration.
Nous recherchons des partenaires académiques partageant notre exigence de rigueur et notre intérêt pour les applications concrètes des méthodes formelles aux systèmes critiques gouvernés.
Quatre modalités
CIFRE
Conventions industrielles de formation par la recherche. Thèses doctorales co-encadrées sur les axes de recherche du CFVL. Financement ANRT + CORTEX AI TM.
Co-encadrement
Doctorats et post-doctorats en méthodes formelles appliquées. Sujets prioritaires : gouvernance formelle, bornage TCB, chaîne de raffinement multi-niveaux.
Publications conjointes
Articles et communications dans les conférences et journaux de référence : ITP, CPP, POPL, CAV, FM, S&P, CCS.
ANR / France 2030
Participation conjointe à des appels à projets en recherche appliquée : cybersécurité, méthodes formelles, IA de confiance, souveraineté numérique.
Sujets de recherche
Gouvernance IA formellement vérifiée
Formalisation des propriétés de gouvernance décisionnelle : non-contournabilité, human-in-the-loop prouvé, séparation décision/action/preuve. Application aux systèmes d’IA critique.
Raffinement et compilation vérifiée
Chaîne continue de la spécification abstraite Isabelle/HOL à l’implémentation C compilée CompCert. Pont AutoCorres. Préservation des propriétés de sécurité à travers les niveaux d’abstraction.
Composition sécurisée
Théorie de la composition pour architectures hiérarchisées. Comment les preuves individuelles des composants TCB se combinent-elles en une garantie système globale ?
Cryptographie formelle post-quantique
Vérification formelle des primitives cryptographiques en contexte post-quantique. Modélisation des menaces quantiques et analyse de résistance des protocoles PRISM™.
Domaines de compétence recherchés
Méthodes formelles
Proof assistants (Isabelle, Coq, Lean), model checking, abstract interpretation, theorem proving. Laboratoires : INRIA, LMF, IRIF, VERIMAG.
Sécurité systèmes
Isolation, non-interférence, microkernels vérifiés, architectures de confiance. Programmes : seL4, CertiKOS, Komodo.
Compilation vérifiée
CompCert, CakeML, traduction certifiée, préservation de propriétés. Programmes : ANR CompCert, MSR F*.
Cryptographie formelle
ProVerif, Tamarin, HACL*, vérification de protocoles, analyse side-channel, post-quantique.
CFVL-REC-003 · Collaborations · Version 1.0 · Février 2026