CVE-2026-72705

Nome do Software Vulnerável e Versões Afetadas Rocq Prover versões anteriores a 9.2.0

Descrição O verificador de guarda (guard checker) não rastreia chamadas recursivas feitas por meio dos próprios argumentos de um fixpoint. Isso ocorre quando um fixpoint passa a si mesmo como um argumento de ordem superior para um segundo fixpoint, que então o aplica a um valor que não é um subtermo do argumento estrutural. Enquanto a passagem de uma função recursiva para uma definição simples é rejeitada porque o verificador desdobra a definição, a passagem para um fixpoint é aceita. Essa falha permite um tipo que é definicionalmente igual à sua própria negação, permitindo que a autoaplicação produza False em código puramente definicional, sem o uso de táticas, axiomas, plugins ou sinalizações inseguras.

Recomendações Atualize o Rocq Prover para a versão 9.2.0.