CVE-2026-72714

Resumo

O Rocq Prover não restaura a cópia da flag de verificação de universos pertencente ao grafo de universos quando um módulo que desativou localmente a verificação é fechado. Espera-se que o comando local Unset Universe Checking dentro de um módulo dure apenas até o fim do módulo, e a flag global seja restaurada, mas o grafo de universos mantém a sua própria cópia, que fica desativada. As duas visões passam então a divergir: o Test Universe Checking reporta a verificação como ativada, enquanto o kernel continua a aceitar termos inconsistentes em termos de universos. Com a restrição entre dois universos deixando de ser imposta, aplica-se o paradoxo de Hurkens, que produz uma prova de False, a partir da qual qualquer proposição se segue. A prova não utiliza axiomas, plugins ou funcionalidades inseguras depois de o módulo ter sido fechado, e o Print Assumptions reporta-a como fechada sob o contexto global, pelo que nem a auditoria de assunções nem a consulta da flag refletem o estado real do kernel. Não existe correção disponível.

Fontes

• rocq-cve-poc-22287PoC

  CVE-2026-72714 — Estado de verificação de universo do Rocq dessincronizado após o fechamento do módulo