Por qué Rocq es mejor que Lean para la verificación de programas

• Aunque el crecimiento de Lean en la formalización matemática es evidente, para la verificación de programas ejecutables encaja mejor Rocq, que cuenta con coinducción nativa, diversas rutas de extracción y un ecosistema de verificación consolidado
• Rocq declara codatos con CoInductive y CoFixpoint, verifica la guardedness y luego los extrae como código de ejecución diferida; en Lean, en cambio, hay que elegir entre una codificación de biblioteca, iteradores, Thunk o partial def
• El verificador de tipos inductivos anidados de Lean rechaza algunas relaciones de verificación que Rocq sí permite, por lo que en el caso de esquemas JSON hay que separar una prueba de Forall₂ en varias relaciones y preparar un principio inductivo aparte
• Rocq ofrece rutas de extracción de programas hacia OCaml, Haskell, Rust, C++, WebAssembly, entre otros, y bases de verificación como Iris, CompCert e Interaction Trees, lo que permite conectar la lógica verificada de un juego real con código ejecutable
• Los agentes de IA también pueden escribir código Rocq si cuentan con documentación y casos; para pasar a Lean habría que reemplazar no solo definiciones, sino también el pipeline de extracción, bibliotecas y antecedentes regulatorios e institucionales, así que en el trabajo actual falta beneficio práctico

---

Comparación desde el criterio de verificación de programas

• El objeto de comparación no es la formalización matemática, sino la verificación de programas, y en el campo de las matemáticas Lean sí tiene un impulso real de crecimiento
• “Mejor” no implica una superioridad absoluta, sino que Rocq se adapta mejor al trabajo que se está realizando actualmente
• Con el aumento de los logros de la IA en matemáticas y el interés por Lean, surgieron preguntas frecuentes sobre por qué se sigue usando Rocq, y el argumento parte de las diapositivas de una keynote de LangSec

Tipos coinductivos nativos y cofixpoint

• Alcance de lo que ofrece coinductive en Lean

  • El soporte para predicados coinductivos, desarrollado por Wojciech Różowski y Joachim Breitner de Lean FRO, está incluido en el comando coinductive de Lean 4.25
  • Esta función es útil para bisimulation y pruebas coinductivas, pero no proporciona cofixpoints ejecutables en Type ni programas extraíbles
  • CoInductive y CoFixpoint de Rocq proporcionan codatos (codata) ejecutables directamente en Type
  • Lean no tiene una declaración de kernel equivalente, por lo que hay que usar funciones y estructuras comunes o codificaciones de biblioteca

• Restricciones de declaración de QPFTypes

  • QPFTypes, de Alex Keizer, es un paquete de prueba de concepto para codatos generales que genera destructores, corecursores y principios de bisimulation a partir de especificaciones codata
  • A diferencia de CoInductive de Rocq, es una codificación de biblioteca, no una declaración del kernel
  • Los ejemplos usan una toolchain fijada en Lean 4.25.0, la versión con soporte más reciente en ese momento
  • En Rocq, las siguientes tres declaraciones comunes no funcionan en QPFTypes
    • Los codatos sin parámetros fallan por un bug de implementación
    • Las declaraciones coinductivas mutuas, como tree y forest, no son compatibles por las restricciones de los bloques mutual de Lean
    • Las familias coinductivas indexadas como istream, en las que el índice de clock avanza en cada paso, no son compatibles por una limitación del propio QPF
  • Los patrones coinductivos indexados también se usan en protocolos, etapas, tamaños y máquinas de estados, pero si uno sale del alcance simple, no mutuo y no indexado de QPFTypes, debe usar directamente las API de bajo nivel MvQPF.Cofix.corec y bisim, o no puede implementarlo
  • El verificador de guardedness de Rocq también es difícil de manejar, pero los casos anteriores se pueden declarar sin codificación adicional
  • Paco y coinduction, de Damien Pous, dan soporte a predicados coinductivos y pruebas de relaciones, pero no reemplazan CoFixpoint para programas

• Diferencias en los programas extraídos

  • Los cofixpoints nativos de Rocq se extraen como verdaderos valores OCaml diferidos
  • unfold_cotree de la biblioteca game tree se convierte en un árbol envuelto en Lazy.t y en una función generadora diferida recursiva
  • El resultado se parece a una estructura de árbol diferida que una persona podría escribir a mano
  • En QPFTypes, la generación y la observación pasan por MvQPF.Cofix.corec y MvQPF.Cofix.dest, y el programa extraído también conserva la representación generalizada de Cofix
  • BadCoinduction.lean contiene Colist, Cotree, las interfaces generadas, casos de falla de codatos sin parámetros, mutuos e indexados, y el commit y los comandos de QPFTypes para reproducirlos

Alternativas que se pueden elegir en Lean

• Streams e iteradores

  • Stream' de mathlib es una función Nat → α
  • Permite calcular el elemento en la posición n y ofrece corecursor, extensionalidad, bisimulación y lemas auxiliares de coinducción
  • Sin embargo, no es un constructor perezoso cuya cola sea otro stream, y tampoco resuelve codatos arbitrarios mutuos o indexados
  • Una máquina de estados con estado explícito y una función step también puede cumplir el rol de corecursor
  • Iter de Lean es una interfaz secuencial que calcula un paso a la vez bajo demanda
  • Los iteradores pueden tener una prueba Productive que garantiza la producción de un valor o la terminación, y Iter.repeat ya la incluye
  • En iteradores definidos por el usuario, hay que proporcionar directamente la interfaz step, los invariantes y, si hace falta, la prueba de productividad
  • CoFixpoint de Rocq revisa la guardedness de las llamadas recursivas y devuelve un valor coinductivo sin trabajo adicional para conectar máquinas de estados y secuencias

• Thunk, partial def, unsafe def

  • Thunk de Lean calcula cuando se fuerza por primera vez en el código compilado y guarda el resultado en caché, pero no ofrece coinducción
  • En la lógica se ve como Unit → α, por lo que la definición completa puede usarse en pruebas, pero la caché no es visible
  • Tampoco permite recursión ni verifica si la recursión acaba produciendo un constructor
  • El código extraído de Rocq también usa pereza en tiempo de ejecución, pero primero pasa una verificación de guardedness
  • partial def permite ejecutar el cuerpo recursivo, pero en la lógica solo queda una constante opaca
  • No verifica terminación ni productividad, así que permite tanto productores de números naturales como productores que entran de inmediato en recursión infinita
  • unsafe def también puede ejecutarse, pero no puede referenciarse en declaraciones theorem-safe
  • MLList de Batteries combina una implementación perezosa unsafe privada, una interfaz pública opaca y productores fix e iterate escritos con partial def
  • Estos productores no pueden desplegarse en pruebas como un cofixpoint de Rocq observado
  • partial_fixpoint conserva las ecuaciones, pero no acepta recursión que combine constructores y thunks
  • QPFTypes evita la opacidad al ofrecer principios de corecursor y bisimulación, pero exige aceptar una representación Cofix generalizada y restricciones de declaración

Programas con efectos que no terminan

• Interaction Trees representa programas con efectos que pueden no terminar como árboles coinductivos
  • Con el mismo árbol se puede escribir, interpretar y extraer programas, y normalmente demostrar ecuaciones que incluyen weak bisimulation
• Stream' e Iter solo ofrecen secuencias, por lo que no pueden expresar las continuaciones de ramificación necesarias para los efectos
• Si se ejecutan árboles de efectos con Thunk y partial def, los productores recursivos se vuelven opacos para las pruebas; para soportar cálculo y pruebas a la vez, hace falta una codificación de biblioteca de codatos
• lean4-itree de MIT PLV implementa Interaction Trees como la coalgebra final PFunctor.M de Mathlib
• PolyFun agrega handlers, procedimientos recursivos, trazas de ejecución, strong/weak bisimulation y pruebas de leyes de mónadas e iteración
  • En Lean se pueden calcular y probar árboles, pero sigue siendo un M-type codificado como biblioteca
  • No hay declaraciones nativas de codatos, y se mantiene una representación general en lugar de programas perezosos directos
• HITrees tampoco esquiva esta restricción
  • Como Lean no tiene tipos coinductivos nativos, no usa el enfoque coinductivo de Delay monad de ITrees
  • Los árboles son inductivos y la no terminación se convierte en un efecto recursivo de orden superior
  • El cálculo recursivo adquiere significado cuando un handler interpreta el efecto, no como un árbol infinito que pueda observarse y desplegarse
  • Puede ejecutarse con interpretación monádica y probarse con interpretación de máquinas de estados, pero la teoría ecuacional de HITree no ofrece ecuaciones generales de despliegue recursivo
• Rocq admite declaraciones de codatos, productores con guardedness, razonamiento basado en observaciones y extracción directa de código perezoso en un solo flujo

Tipos y predicados inductivos anidados

• Caso de validación de esquemas JSON

  • Lean permite varias definiciones inductivas anidadas, pero rechaza algunas definiciones que Rocq sí acepta
  • Esta diferencia se usó en A Rose Tree Is Blooming, y puede reproducirse con un caso más pequeño de esquemas JSON
  • Tanto JSON como los propios esquemas pueden definirse sin problemas en ambos lenguajes
  • En la validación de esquemas de objetos, hay que comprobar por pares que los nombres de campo coincidan y que cada valor JSON sea válido para su subesquema correspondiente
  • Rocq puede guardar la igualdad de nombres y la validación recursiva en una sola derivación Forall2
  • Rocq 9.0 rechaza como una violación de positividad estricta una lambda con patrón de tupla alrededor de una aparición recursiva, pero compila si se usan proyecciones en lugar de patrones
  • Lean 4.32.1 rechaza erróneamente el And interno como tipo de datos inductivo anidado no válido cuando, en el mismo constructor de objeto, una aparición recursiva pasa tanto por Forall₂ como por And
  • Acepta formas cercanas como Forall₂ ParRed, recursión directa a través de And·Exists, y Forall₂ (fun sf jf => Valid sf.2 jf.2)
  • Forall₂ (Eval env), donde el parámetro de relación captura la variable local del constructor env, falla en la etapa de Forall₂

• Formas de rodearlo y costo de las pruebas

  • En Lean, la validación de objetos puede dividirse en dos derivaciones Forall₂
    • Una conserva la igualdad de los nombres de campo
    • La otra conserva la validación recursiva de los valores correspondientes
  • Sin índices separados ni pruebas de longitud, se puede mantener la estructura de lista y también probar estructuralmente la eliminación de la cabeza, pero hay que descomponer ambas derivaciones
  • Al separar la relación, se pierde el objeto de prueba único en el que cada igualdad de nombre y validación recursiva queda emparejada
  • Se puede restaurar la unión con una relación mutua ValidFields, pero la táctica induction de Lean no admite tipos inductivos mutuos y el recursor generado también exige un motive por cada relación
  • Crear un teorema de inducción personalizado permite ocultar esta configuración
  • Rocq mantiene la representación estándar con Forall2 y, si se necesita una definición mutua, puede generar el principio combinado con Scheme
  • Lean también puede expresar la misma proposición sin una codificación basada en índices, pero hay que reubicar declaraciones y crear más infraestructura de prueba
  • El archivo comparativo completo está en NestedPain.v para Rocq 9.0.0 y NestedPain.lean para Lean 4.32.1; los fallos esperados de Lean se comprueban al compilar con #guard_msgs

• Principios de inducción fuertes para argumentos anidados

  • En pruebas que requieren hipótesis elemento por elemento sobre datos anidados, como cuando Term contiene list Term, ambos sistemas necesitaban un recursor más fuerte
  • Rocq 9.2 genera hipótesis de inducción para argumentos anidados si se registran el predicado All y los teoremas para el nesting type
  • La biblioteca estándar no los registra de forma predeterminada, así que hay que agregar una línea Scheme All for list. antes de declarar Term
  • Los Term_ind y Term_rect generados obtienen la hipótesis list_all Term P l en el caso app, y el cuerpo llama a list_all_forall
  • Si se agrega Scheme All for Forall2., ParRed_ind también proporciona hipótesis de inducción para la premisa Forall2 ParRed args args'
  • Si no se registra, aparece una advertencia [register-all] junto con el principio débil existente
  • En Lean, todavía hay que preparar manualmente un recursor fuerte

Opciones de extracción de programas

• La toolchain estándar de Lean compila mediante su propio runtime, lo que tiene ventajas si se construyen bibliotecas de Lean y el diseño del runtime encaja
• El lean-zip verificado de Kim Morrison incluso puede comprimir más rápido que el miniz_oxide en Rust puro, por lo que su rendimiento es impresionante
• Sin embargo, Lean no ofrece varios backends alternativos de extracción, y su pipeline de compilación actual no cuenta con una prueba de corrección de extremo a extremo
  • Pueden aparecer problemas raros, como el bug de runtime descubierto por Kiran Gopinathan
  • El código generado está especializado para el runtime y no está diseñado para ser leído por personas
• Rocq cuenta con varios caminos que ofrecen distintos compromisos entre base de confianza y legibilidad
  • OCaml·Haskell·Scheme
  • Pipeline de extracción verificado hacia Malfunction
  • Rust
  • Elm
  • Clight y WebAssembly mediante CertiRocq, con algunas partes aún en desarrollo
  • Extracción a C++ con Crane, orientada a generar código legible

Juegos que ejecutan lógica verificada

• En Rocq, después de verificar mecánicamente propiedades del mismo código fuente que el programa ejecutable, se extraen la lógica y el event loop a C++ con Crane y se conectan a SDL2 con rocq-crane-sdl2

• Rocqman

  • Rocqman prueba las transiciones de estado del juego usadas por el frame loop
    • La puntuación no disminuye
    • Las vidas y los coleccionables restantes no aumentan
    • El estado final es un punto fijo de tick
    • Comprueba las transiciones de pausa y de pantalla final

• Rocqsweeper

  • Rocqsweeper prueba las reglas de Minesweeper y la capa de entrada
    • El primer clic es seguro
    • Colocar banderas preserva las minas y los datos de adyacencia
    • El flood fill preserva las minas y no aumenta las casillas seguras ocultas
    • El cursor no sale de los límites
    • Los eventos del mouse se interpretan como la celda esperada

• Reversirocq

  • Reversirocq usa las reglas de Reversi agregadas por Charles C. Norton y la IA alpha-beta coinductiva de la misma game tree library
  • Los teoremas tratan la enumeración de jugadas legales y los resultados de la partida, y conectan alpha-beta con minimax en los prefijos finitos explorados

• Límite de verificación

  • El límite de las pruebas termina en el código fuente de Rocq y no incluye SDL, Crane, el C++ generado ni el runtime nativo
  • Dentro del límite se prueban propiedades de la lógica que realmente se ejecuta, no de un modelo separado del programa ejecutable

Ecosistema de verificación de programas de Rocq

• Abstracciones para representar programas

  • Interaction Trees: representan programas con efectos y que podrían no terminar como árboles coinductivos de eventos externos, y ofrecen semántica denotacional y razonamiento ecuacional para código impuro
  • Choice Trees: agregan elecciones no deterministas internas para modelar sistemas no deterministas, como los concurrentes

• Frameworks de verificación de programas

  • Iris: framework de lógica de separación concurrente de orden superior para programas con estado y concurrentes
  • Iris-Lean también avanza rápido y admite muchas funciones, pero no se ha usado tan ampliamente como Rocq Iris
  • CFML: importa código fuente OCaml a Rocq, genera fórmulas características y ofrece tácticas para especificaciones de lógica de separación de orden superior
  • Perennial: framework basado en Iris para verificar concurrencia, almacenamiento seguro ante fallos y sistemas distribuidos; se conecta con programas ejecutables de un subconjunto de Go mediante Goose
  • VST: Verified Software Toolchain que prueba la corrección funcional de programas en C con base en la semántica de CompCert
  • BRiCk: lógica de programas y toolchain para programas C++ reales

• Herramientas con backend o componentes de Rocq

  • Frama-C: plataforma de análisis y verificación deductiva para C que puede delegar obligaciones de prueba a Rocq
  • Why3: puede enviar objetivos de su propio lenguaje a varios probadores y exportar obligaciones de prueba interactivas para Rocq
  • Cerberus: semántica formal ejecutable de un subconjunto práctico y grande de C, con una implementación en Rocq para el modelo de memoria de CHERI C

• Semánticas de lenguajes reales y compiladores verificados

  • CompCert: compilador optimizador de C verificado formalmente
  • Vellvm: ofrece una especificación en Rocq y semántica abstracta de LLVM IR, además de un intérprete ejecutable probado como refinamiento de esa semántica
  • Vélus: compilador verificado de Lustre a Clight de CompCert
  • WasmCert: semántica formal mecanizada de WebAssembly
  • JSCert: semántica formal de JavaScript que sigue la especificación ECMAScript 5

• Verificación ligera basada en traducción

  • hs-to-coq: traduce código fuente Haskell a Rocq
  • rocq-of-ocaml: traduce código fuente OCaml a Rocq
  • rocq-of-python: traduce código fuente Python a Rocq
  • rocq-of-rust: traduce código fuente Rust a Rocq
  • Aeneas: convierte Rust que pasó el borrow check en un modelo de funciones puras para verificación, y también admite Lean como destino

• Síntesis de programas y parsing

  • Fiat Crypto: deriva, con enfoque correct-by-construction, aritmética criptográfica de alto rendimiento que puede usarse en navegadores y bibliotecas TLS
  • Rupicola: herramienta de compilación relacional que convierte programas Gallina funcionales de bajo nivel en programas imperativos Bedrock2
  • Narcissus: deriva encoders y decoders correct-by-construction para formatos binarios
  • Verbatim: lexer verificado basado en expresiones regulares
  • CoStar: parser verificado basado en el algoritmo ALL(*)

• Estado de mantenimiento

  • Algunos proyectos no se mantienen activamente, pero fue posible encargárselos a un agente para que los volviera a compilar y ejecutar
  • Aunque un componente necesario pueda portarse a Lean en poco tiempo, eso no traslada automáticamente toda la funcionalidad y el historial de uso acumulados por el ecosistema

Regulación e historial de certificación

• No hay experiencia directa de certificación en aceptación regulatoria, un factor que puede ser más importante especialmente para trabajadores en Europa
• La ANSSI de Francia publicó criterios para usar Rocq en evaluaciones Common Criteria
• CompCert afirma que, mediante el trabajo realizado por AbsInt bajo la guía de Airbus, en 2026 logró la qualification para la computadora MFC_NG de los aviones ATR 42/72
• No se sabe qué requisitos tendría que cumplir un port a Lean en el mismo entorno y, aunque el port sea prolijo, no hereda automáticamente el historial de certificación existente

Agentes de IA y costo de transición

• A diferencia de la premisa de que los agentes de IA solo escriben bien Lean, también pueden escribir código Rocq suficientemente bien
• Rocq existe desde fines de la década de 1980, por lo que acumula mucho código y documentación
• Los modelos actuales se adaptan bien incluso a lenguajes que no conocen tanto si se les proporcionan documentación y ejemplos, así que el argumento de que solo conocen lenguajes populares no es una base de largo plazo para cambiar de proof assistant
• En Lean también se están desarrollando trabajos serios de verificación de programas, como mvcgen y Velvet
• Para trasladar el trabajo actual a Lean habría que reconstruir definiciones y reemplazar pipelines de extracción, bibliotecas e historial institucional, por lo que por ahora Rocq es más adecuado