Pourquoi Rocq est meilleur que Lean pour la vérification de programmes

• Si la progression de Lean dans la formalisation des mathématiques est manifeste, Rocq est mieux adapté à la vérification de programmes exécutables, grâce à sa coinduction native, à ses multiples voies d’extraction et à son écosystème de vérification éprouvé
• Rocq permet de déclarer des codonnées avec CoInductive et CoFixpoint, de vérifier la guardedness, puis de les extraire en code à exécution paresseuse ; avec Lean, il faut choisir entre un encodage en bibliothèque, des itérateurs, Thunk ou partial def
• Le vérificateur de types inductifs imbriqués de Lean rejette certaines relations de vérification que Rocq autorise ; dans le cas des schémas JSON, il faut scinder une preuve Forall₂ en plusieurs relations et mettre en place un principe d’induction séparé
• Rocq offre des voies d’extraction de programmes vers OCaml, Haskell, Rust, C++, WebAssembly, etc., ainsi que des bases de vérification comme Iris, CompCert et Interaction Trees, ce qui permet de relier la logique vérifiée de jeux réels à du code exécutable
• Les agents IA peuvent eux aussi écrire du code Rocq s’ils disposent de documentation et d’exemples ; passer à Lean impliquerait de remplacer non seulement les définitions, mais aussi le pipeline d’extraction, les bibliothèques, ainsi que l’historique réglementaire et institutionnel, si bien que le gain pratique est aujourd’hui insuffisant pour le travail en cours

---

Comparaison du point de vue de la vérification de programmes

• La comparaison ne porte pas sur la formalisation des mathématiques, mais sur la vérification de programmes ; dans le domaine des mathématiques, Lean dispose d’une véritable dynamique de croissance
• « Meilleur » ne signifie pas une supériorité absolue, mais que Rocq convient mieux au travail actuellement mené
• Avec les progrès de l’IA en mathématiques et l’intérêt croissant pour Lean, la question de savoir pourquoi continuer à utiliser Rocq revient souvent ; l’argumentation part de diapositives présentées lors d’une keynote LangSec

Types coinductifs natifs et cofixpoint

• Ce que fournit coinductive dans Lean

  • Le support des prédicats coinductifs développé par Wojciech Różowski et Joachim Breitner de Lean FRO est inclus dans la commande coinductive de Lean 4.25
  • Cette fonctionnalité est utile pour la bisimulation et les preuves coinductives, mais ne fournit pas de cofixpoint exécutable dans Type ni de programme extractible
  • CoInductive et CoFixpoint de Rocq fournissent directement dans Type des codonnées (codata) exécutables
  • Lean ne possède pas de déclaration correspondante dans le noyau ; il faut donc utiliser des fonctions et structures ordinaires, ou un encodage en bibliothèque

• Contraintes de déclaration de QPFTypes

  • QPFTypes d’Alex Keizer est un paquet de preuve de concept pour des codonnées générales, qui génère des destructeurs, des corécursseurs et des principes de bisimulation à partir d’une spécification codata
  • Contrairement au CoInductive de Rocq, il s’agit d’un encodage en bibliothèque, pas d’une déclaration du noyau
  • Les exemples utilisent une chaîne d’outils figée sur Lean 4.25.0, la version la plus récente prise en charge à ce moment-là
  • Dans Rocq, les trois déclarations ordinaires suivantes ne fonctionnent pas avec QPFTypes
    • Les codonnées sans paramètre échouent à cause d’un bug d’implémentation
    • Les déclarations mutuellement coinductives comme tree et forest ne sont pas prises en charge en raison des contraintes des blocs mutual de Lean
    • Les familles coinductives indexées comme istream, où l’indice d’horloge progresse à chaque étape, ne sont pas prises en charge en raison d’une limite propre à QPF
  • Les protocoles, les phases, les tailles et les machines à états utilisent eux aussi des motifs de coinduction indexée, mais dès que l’on sort du périmètre simple, non mutuel et non indexé de QPFTypes, il faut utiliser directement les API bas niveau MvQPF.Cofix.corec et bisim, ou bien l’implémentation devient impossible
  • Rocq aussi impose de composer avec un vérificateur de guardedness difficile à manier, mais les cas ci-dessus peuvent y être déclarés sans encodage supplémentaire
  • Paco et coinduction de Damien Pous prennent en charge les prédicats coinductifs et les preuves de relations, mais ne remplacent pas CoFixpoint pour les programmes

• Différences entre les programmes extraits

  • Les cofixpoints natifs de Rocq sont extraits en véritables valeurs OCaml paresseuses
  • unfold_cotree de la bibliothèque game tree devient un arbre enveloppé dans Lazy.t et une fonction de génération paresseuse récursive
  • Le résultat est proche d’une structure d’arbre paresseuse qu’un humain pourrait écrire directement
  • Avec QPFTypes, la génération et l’observation passent par MvQPF.Cofix.corec et MvQPF.Cofix.dest, et le programme extrait conserve lui aussi une représentation généralisée Cofix
  • BadCoinduction.lean contient Colist, Cotree, les interfaces générées, les cas d’échec des codonnées sans paramètre, mutuelles et indexées, ainsi que le commit QPFTypes et les commandes permettant de les reproduire

Les alternatives possibles dans Lean

• Streams et itérateurs

  • Le Stream' de mathlib est une fonction Nat → α
  • Il permet de calculer l’élément à la position n et fournit des lemmes auxiliaires de corecursion, d’extensionalité, de bisimulation et de coinduction
  • Mais ce n’est pas un constructeur paresseux dont la queue est un autre stream, et il ne résout pas les codonnées mutuelles ou indexées arbitraires
  • Une machine à états utilisant un état explicite et une fonction step peut aussi jouer le rôle de corecurseur
  • L’Iter de Lean est une interface séquentielle qui calcule une étape à la demande
  • Les itérateurs peuvent disposer d’une preuve Productive, garantissant qu’ils produisent une valeur ou se terminent ; Iter.repeat en fournit déjà une
  • Pour les itérateurs personnalisés, il faut fournir soi-même l’interface step, les invariants et, si nécessaire, la preuve de productivité
  • Le CoFixpoint de Rocq vérifie la guardedness des appels récursifs et renvoie une valeur coinductive, sans travail séparé de connexion entre machine à états et séquence

• Thunk, partial def, unsafe def

  • Le Thunk de Lean calcule dans le code compilé lors de la première contrainte et met le résultat en cache, mais ne fournit pas de coinduction
  • Dans la logique, il apparaît comme Unit → α, ce qui permet d’utiliser la définition complète dans les preuves, mais le cache n’est pas visible
  • Il n’autorise pas non plus la récursion et ne vérifie pas si la récursion finit par produire un constructeur
  • Le code extrait de Rocq utilise lui aussi de la paresse à l’exécution, mais il passe d’abord la vérification de guardedness
  • partial def permet d’exécuter un corps récursif, mais ne laisse dans la logique qu’une constante opaque
  • Il ne vérifie ni la terminaison ni la productivité, et accepte aussi bien un producteur de nombres naturels qu’un producteur qui boucle immédiatement à l’infini
  • unsafe def peut également être exécuté, mais ne peut pas être référencé dans des déclarations sûres pour les théorèmes
  • Le MLList de Batteries combine une implémentation paresseuse unsafe privée, une interface publique opaque, et des producteurs fix et iterate écrits avec partial def
  • Ces producteurs ne peuvent pas être dépliés dans les preuves comme un cofixpoint Rocq observé
  • partial_fixpoint conserve les équations, mais n’accepte pas la récursion combinant constructeurs et thunks
  • QPFTypes évite l’opacité en fournissant des principes de corecursion et de bisimulation, mais impose une représentation Cofix généralisée et des contraintes de déclaration

Programmes avec effets et non terminants

• Les Interaction Trees représentent les programmes avec effets et potentiellement non terminants sous forme d’arbres coinductifs
  • On peut écrire, interpréter et extraire des programmes avec le même arbre, et prouver des équations, généralement jusqu’à la weak bisimulation incluse
• Stream' et Iter ne fournissent que des séquences et ne peuvent donc pas représenter les continuations de branchement nécessaires aux effets
• Si l’on exécute des arbres d’effets avec Thunk et partial def, les producteurs récursifs deviennent opaques dans les preuves ; pour prendre en charge à la fois le calcul et les preuves, il faut un encodage de bibliothèque de codonnées
• lean4-itree du MIT PLV implémente les Interaction Trees avec la coalgebra finale PFunctor.M de Mathlib
• PolyFun ajoute des handlers, des procédures récursives, des traces d’exécution, des bisimulations strong/weak, ainsi que des preuves des lois de monade et d’itération
  • Il permet de calculer et de prouver sur les arbres dans Lean, mais cela reste un M-type encodé en bibliothèque
  • Il n’existe pas de déclaration native de codonnées, et une représentation générique est conservée au lieu d’un programme paresseux direct
• HITrees ne contourne pas non plus cette contrainte
  • Comme Lean n’a pas de types coinductifs natifs, il n’utilise pas l’approche par monade Delay coinductive des ITrees
  • Les arbres sont inductifs, et la non-terminaison devient un effet récursif d’ordre supérieur
  • Le calcul récursif prend sens lorsque le handler interprète l’effet, plutôt que comme un arbre infini observable et dépliable
  • On peut exécuter par interprétation monadique et prouver par interprétation en machine à états, mais la théorie équationnelle des HITree ne fournit pas d’équations générales de dépliage récursif
• Rocq prend en charge, dans un même flux, les déclarations de codonnées, les producteurs gardés, le raisonnement par observation et l’extraction directe de code paresseux

Types et prédicats inductifs imbriqués

• Exemple de validation de schéma JSON

  • Lean autorise plusieurs définitions inductives imbriquées, mais rejette certaines définitions acceptées par Rocq
  • Cette différence a été utilisée dans A Rose Tree Is Blooming, et peut être reproduite avec un exemple plus petit de schéma JSON
  • JSON et les schémas eux-mêmes peuvent être définis sans problème dans les deux langages
  • Pour valider un schéma d’objet, il faut vérifier paire par paire que les noms de champs correspondent et que chaque valeur JSON est valide pour le sous-schéma correspondant
  • Rocq peut stocker l’égalité des noms et la validation récursive dans une seule dérivation Forall2
  • Rocq 9.0 rejette les lambdas à motif de tuple autour des occurrences récursives comme une violation de positivité stricte, mais le code compile si l’on utilise des projections au lieu de motifs
  • Lean 4.32.1 rejette à tort le And interne comme type de données inductif imbriqué non valide lorsque, dans le même constructeur d’objet, l’occurrence récursive passe à la fois par Forall₂ et par And
  • Des formes voisines comme Forall₂ ParRed, la récursion directe via And·Exists, ou Forall₂ (fun sf jf => Valid sf.2 jf.2) sont acceptées
  • Forall₂ (Eval env), où le paramètre de relation capture la variable locale de constructeur env, échoue à l’étape Forall₂

• Contournements et coût des preuves

  • Dans Lean, la validation d’objet peut être scindée en deux dérivations Forall₂
    • l’une préserve l’égalité des noms de champs
    • l’autre préserve la validation récursive des valeurs correspondantes
  • On peut conserver la structure de liste et prouver structurellement la suppression de la tête sans index séparés ni preuves de longueur, mais il faut décomposer les deux dérivations
  • Séparer les relations fait perdre l’objet de preuve unique où chaque égalité de nom et chaque validation récursive sont regroupées par paire
  • On peut rétablir ce couplage avec une relation mutuelle ValidFields, mais la tactique induction de Lean ne prend pas en charge les types inductifs mutuels, et le récurseur généré demande aussi un motif pour chaque relation
  • Créer un théorème d’induction personnalisé permet de masquer cette configuration
  • Rocq conserve la représentation standard Forall2 et, si une définition mutuelle est nécessaire, peut générer le principe combiné avec Scheme
  • Lean peut lui aussi exprimer la même proposition sans encodage fondé sur des index, mais il faut réorganiser les déclarations et créer davantage d’outillage de preuve
  • Les fichiers complets de comparaison sont NestedPain.v pour Rocq 9.0.0 et NestedPain.lean pour Lean 4.32.1 ; les échecs attendus de Lean sont vérifiés à la compilation avec #guard_msgs

• Principes d’induction forts pour les arguments imbriqués

  • Pour les preuves qui nécessitent des hypothèses élément par élément sur des données imbriquées, comme lorsque Term contient list Term, les deux systèmes avaient besoin d’un récurseur plus fort
  • Rocq 9.2 génère des hypothèses d’induction pour les arguments imbriqués si l’on enregistre un prédicat All et des théorèmes pour le type imbriquant
  • La bibliothèque standard ne les enregistre pas par défaut ; il faut donc ajouter la ligne Scheme All for list. avant la déclaration de Term
  • Les Term_ind et Term_rect générés obtiennent, dans le cas app, une hypothèse list_all Term P l, et le corps appelle list_all_forall
  • Ajouter Scheme All for Forall2. permet aussi à ParRed_ind de fournir des hypothèses d’induction pour la prémisse Forall2 ParRed args args'
  • Sans enregistrement, un avertissement [register-all] apparaît avec l’ancien principe faible
  • Dans Lean, il faut toujours fournir soi-même un récurseur fort

Options d’extraction de programmes

• La chaîne d’outils standard de Lean compile via son propre runtime, ce qui est avantageux lorsque l’on crée des bibliothèques Lean et que la conception du runtime convient
• Le lean-zip vérifié de Kim Morrison peut même compresser plus vite que le pur Rust miniz_oxide, ce qui est impressionnant en termes de performance
• Cependant, Lean ne propose pas plusieurs backends d’extraction alternatifs, et son pipeline de compilation actuel ne dispose pas d’une preuve de correction de bout en bout
  • Des problèmes rares peuvent survenir, comme le bug de runtime découvert par Kiran Gopinathan
  • Le code généré est spécialisé pour le runtime et n’est pas conçu pour être lu par des humains
• Rocq dispose de plusieurs voies offrant différents compromis entre base de confiance et lisibilité
  • OCaml·Haskell·Scheme
  • pipeline d’extraction vérifié vers Malfunction
  • Rust
  • Elm
  • Clight et WebAssembly via CertiRocq, dont certaines parties sont en cours de développement
  • extraction C++ de Crane, qui vise un code généré lisible

Jeux exécutant de la logique vérifiée

• Dans Rocq, après avoir vérifié mécaniquement des propriétés du même code source que le programme exécutable, la logique et la boucle d’événements sont extraites en C++ avec Crane et connectées à SDL2 via rocq-crane-sdl2

• Rocqman

  • Rocqman prouve les transitions d’état de jeu utilisées par la boucle de frames
    • le score ne diminue pas
    • les vies et les objets à collecter restants n’augmentent pas
    • l’état de fin est un point fixe de tick
    • les transitions vers pause et écran de fin sont vérifiées

• Rocqsweeper

  • Rocqsweeper prouve les règles de Minesweeper et la couche d’entrée
    • le premier clic est sûr
    • le marquage par drapeau préserve les données de mines et d’adjacence
    • le flood fill préserve les mines et n’augmente pas les cases sûres cachées
    • le curseur ne sort pas des limites
    • les événements souris sont interprétés comme les cellules attendues

• Reversirocq

  • Reversirocq utilise les règles de Reversi ajoutées par Charles C. Norton et l’IA alpha-bêta coinductive de la même bibliothèque de game trees
  • Les théorèmes portent sur l’énumération des coups légaux et les résultats de partie, et relient alpha-bêta à minimax sur le préfixe fini exploré

• Limite de vérification

  • La limite de preuve s’arrête au source Rocq et n’inclut pas SDL, Crane, le C++ généré ni le runtime natif
  • À l’intérieur de cette limite, les propriétés prouvées sont celles de la logique réellement exécutée, et non celles d’un modèle séparé du programme exécutable

Écosystème de vérification de programmes avec Rocq

• Abstractions pour représenter les programmes

  • Interaction Trees : représentent des programmes à effets, susceptibles de ne pas terminer, sous forme d’arbres coinductifs d’événements externes, et fournissent une sémantique dénotationnelle ainsi qu’un raisonnement équationnel pour le code impur
  • Choice Trees : ajoutent des choix non déterministes internes pour modéliser des systèmes non déterministes, comme ceux impliquant de la concurrence

• Frameworks de vérification de programmes

  • Iris : framework de logique de séparation concurrente d’ordre supérieur pour les programmes à état et concurrents
  • Iris-Lean évolue aussi rapidement et prend en charge de nombreuses fonctionnalités, mais n’a pas été utilisé aussi largement qu’Iris pour Rocq
  • CFML : importe du code source OCaml dans Rocq, génère des formules caractéristiques et fournit des tactiques pour les spécifications en logique de séparation d’ordre supérieur
  • Perennial : framework fondé sur Iris pour vérifier la concurrence, les stockages résistants aux crashs et les systèmes distribués ; il relie des programmes exécutables d’un sous-ensemble de Go via Goose
  • VST : Verified Software Toolchain, qui prouve la correction fonctionnelle de programmes C à partir de la sémantique de CompCert
  • BRiCk : logique de programme et chaîne d’outils pour de vrais programmes C++

• Outils dotés d’un backend ou de composants Rocq

  • Frama-C : plateforme d’analyse et de vérification déductive du C, capable de transmettre des obligations de preuve à Rocq
  • Why3 : peut envoyer les objectifs de son propre langage à plusieurs prouveurs et exporter des obligations de preuve interactives pour Rocq
  • Cerberus : sémantique formelle exécutable d’un grand sous-ensemble pratique de C, avec une implémentation Rocq du modèle mémoire CHERI C

• Sémantiques de langages réels et compilateurs vérifiés

  • CompCert : compilateur C optimisant formellement vérifié
  • Vellvm : fournit une spécification Rocq et une sémantique abstraite de LLVM IR, ainsi qu’un interpréteur exécutable prouvé par raffinement de cette sémantique
  • Vélus : compilateur vérifié de Lustre vers Clight de CompCert
  • WasmCert : sémantique formelle mécanisée de WebAssembly
  • JSCert : sémantique formelle de JavaScript qui suit la spécification ECMAScript 5

• Vérification légère fondée sur la traduction

  • hs-to-coq : traduit du code source Haskell vers Rocq
  • rocq-of-ocaml : traduit du code source OCaml vers Rocq
  • rocq-of-python : traduit du code source Python vers Rocq
  • rocq-of-rust : traduit du code source Rust vers Rocq
  • Aeneas : transforme du Rust ayant passé le borrow check en modèles de fonctions pures destinés à la vérification, et prend aussi Lean comme cible

• Synthèse de programmes et parsing

  • Fiat Crypto : dérive, selon une approche correct-by-construction, de l’arithmétique cryptographique haute performance pouvant être utilisée dans les navigateurs et les bibliothèques TLS
  • Rupicola : outil de compilation relationnelle qui transforme des programmes Gallina fonctionnels de bas niveau en programmes impératifs Bedrock2
  • Narcissus : dérive des encodeurs et décodeurs correct-by-construction pour formats binaires
  • Verbatim : lexer vérifié fondé sur les expressions régulières
  • CoStar : parser vérifié fondé sur l’algorithme ALL(*)

• État de maintenance

  • Certains projets ne sont plus activement maintenus, mais il a été possible de les confier à des agents pour les reconstruire et les exécuter à nouveau
  • Même si un élément nécessaire peut être porté vers Lean en peu de temps, cela ne transfère pas automatiquement l’ensemble des fonctionnalités et de l’historique d’usage accumulés par tout l’écosystème

Réglementation et historique de certification

• Il n’existe pas d’expérience directe de certification pour l’acceptation réglementaire, un facteur qui peut être particulièrement important pour les acteurs européens
• L’ANSSI française a publié des exigences pour l’utilisation de Rocq dans le cadre d’évaluations Common Criteria
• CompCert indique avoir été qualifié avec succès en 2026 pour l’ordinateur MFC_NG des avions ATR 42/72, via des travaux menés par AbsInt sous la direction d’Airbus
• On ne sait pas quelles exigences un port Lean devrait satisfaire dans le même environnement, et même un portage propre n’hérite pas automatiquement de l’historique de certification existant

Agents IA et coût de migration

• Contrairement à l’hypothèse selon laquelle les agents IA n’écriraient bien que du Lean, ils peuvent aussi écrire du code Rocq de manière tout à fait satisfaisante
• Rocq existe depuis la fin des années 1980, avec une grande quantité de code et de documentation accumulée
• Les modèles actuels s’adaptent bien même à des langages qui leur sont moins familiers lorsqu’on leur fournit de la documentation et des exemples ; la seule familiarité avec les langages populaires ne constitue donc pas une raison durable de changer de proof assistant
• Des travaux sérieux de vérification de programmes sont également en cours avec Lean, notamment mvcgen et Velvet
• Migrer le travail actuel vers Lean supposerait de reconstruire les définitions et de remplacer le pipeline d’extraction, les bibliothèques et l’historique institutionnel ; à ce stade, Rocq est donc plus adapté