CVE-2026-72714

Resumen

Rocq Prover no restaura la copia del grafo de universos del indicador de verificación de universos cuando se cierra un módulo que deshabilitó localmente la verificación. Se espera que la desactivación local de la verificación de universos dentro de un módulo dure solo hasta que el módulo finalice y el indicador global sea restaurado, pero el grafo de universos mantiene su propia copia, que queda deshabilitada. Las dos vistas entonces discrepan: Test Universe Checking informa que la verificación está habilitada mientras que el kernel continúa aceptando términos inconsistentes con los universos. Al no aplicarse ya la restricción entre dos universos, la paradoja de Hurkens se aplica y produce una prueba de Falso, de la cual se deduce cualquier proposición. La prueba no utiliza axiomas, plugins ni características inseguras una vez que el módulo se ha cerrado, y Print Assumptions lo reporta como cerrado bajo el contexto global, por lo que ni la auditoría de suposiciones ni la consulta del indicador reflejan el estado real del kernel. No hay solución disponible.

Fuentes

• rocq-cve-poc-22287PoC

  CVE-2026-72714 — Estado de comprobación del universo Rocq desincronizado tras el cierre del módulo