Vérification formelle
Fellow suit ce sujet depuis juillet 2026 : 12 articles résumés en français, dont 4 jugés majeurs ou notables.
Les sorties majeures
Les LLM rendent la vérification formelle de logiciels faisable à bien plus grande échelle
Preuves formelles de non-crash produites par Claude pour 239 points d'entrée dans 123 bibliothèques open source, publiées en partie et vérifiables, avec bugs corrigés et pipeline proposé par Theorem.
Un défi mathématique vieux de 31 ans résolu : la conjecture KLS
Preuve d'une conjecture ouverte depuis 31 ans, confirmée par des preuves indépendantes parallèles et une formalisation Lean 4, qui rend inconditionnels de nombreux résultats dépendants de KLS.
Toute l'actualité · 12 articles
Les LLM rendent la vérification formelle de logiciels faisable à bien plus grande échelle
Avec Theorem, Anthropic a utilisé Claude pour prouver des propriétés de sécurité au niveau assembleur RISC-V dans plus de 100 bibliothèques open source réelles.
Un défi mathématique vieux de 31 ans résolu : la conjecture KLS
Un chercheur de Microsoft et un collaborateur résolvent la conjecture KLS, problème central de la géométrie en grande dimension, grâce à une recherche pilotée par des humains et assistée par des agents IA.
Que mesurent réellement les benchmarks de réparation de RTL ?
Une étude construit RTLRepairBench et un jeu d'entraînement, puis met en évidence deux biais de mesure : sémantique de reset en simulation versus formel, et rôle de la spécification seule.
Ship Your Interpreter : des LLMs pour écrire et vérifier la sémantique formelle d'un langage
Basis montre que des LLMs peuvent rédiger la sémantique formelle d'un petit langage, puis prouver sous Lean que son interpréteur la respecte, jusqu'au code RISC-V compilé.
Cogentic : une orchestration multi-agents pour la découverte automatisée de preuves
Un système multi-agents basé sur Gemini combine preuve et vérification itératives pour résoudre des problèmes mathématiques ouverts.
Commissionnement vérifié par exigences : un modèle local gelé de 4B paramètres comme générateur de candidats sous couche de validation externe
Un protocole de validation sépare la génération de candidats de l'autorité de release. Un LLM local de 4B est encadré par une porte logique externe scellée pour garantir la fiabilité des plans en commissionnement mécatronique.
EquivSVA : un dataset formellement vérifié d'assertions comportementales sur des implémentations RTL équivalentes
Un nouveau dataset évalue si les assertions SystemVerilog générées par LLM capturent le comportement observable, indépendamment des détails d'implémentation RTL.
IA sous vérification formelle : de l'application au silicium
Un chercheur affirme avoir dirigé une flotte d'agents IA, sans aucune revue humaine des preuves, jusqu'à un processeur RISC-V gravé.
Vero : des agents IA capables de construire des dépôts logiciels formellement vérifiés ?
Un nouveau benchmark évalue si les agents IA peuvent produire, à l'échelle d'un dépôt entier, du code et des preuves formelles cohérents.
Comment vérifier la cohérence d'affirmations probabilistes
Un protocole de preuve interactive permet de vérifier en temps polynomial la cohérence des prédictions probabilistes d'un modèle d'IA, avec des implications pour la sécurité.
Show HN : un DSL Datalog en Lean4 inspiré de Google Zanzibar pour projets IA
Un développeur présente une bibliothèque Lean4 permettant de définir des règles d'autorisation façon Zanzibar, formellement vérifiables.
Show HN : CSG 3D formellement vérifié — faire confiance à une spec de 93 lignes, pas à 1000 lignes de code IA
Un projet open source propose une bibliothèque d'intersection de maillages 3D avec preuve formelle, plutôt qu'un code généré par IA non vérifié.