Gaëtan Gilbert

**Nome do Software Vulnerável e Versões Afetadas** Rocq Prover (versões afetadas não especificadas) **Descrição** O software não restaura a cópia da flag de verificação de universo do grafo de universos após o fechamento de um módulo que desativou a verificação localmente. Embora a flag global seja restaurada, o grafo de universos mantém o estado desativado, causando uma discrepância onde o sistema relata que a verificação está ativada enquanto o kernel continua a aceitar termos inconsistentes de universo. Isso permite a aplicação do paradoxo de Hurkens—uma contradição lógica—para produzir uma prova de Falso, permitindo que qualquer proposição seja provada. Este estado persiste mesmo sem o uso de axiomas, plugins ou recursos inseguros, e não é refletido na auditoria de suposições ou nas consultas de flag. **Recomendações** No momento, não há informações sobre uma versão mais recente que contenha a correção para esta vulnerabilidade.