CVE-2026-72711

Nome do Software Vulnerável e Versões Afetadas Lean 4 versões anteriores a 4.32.2

Descrição O kernel não verifica se o corpo de uma declaração opaca está fechado. Especificamente, a função environment::add opaque omite a chamada check no metavar no fvar() utilizada nos caminhos de definição e teorema, permitindo que valores com variáveis livres ausentes do contexto local sejam aceitos. Um metaprograma pode explorar isso criando um local temporário do tipo False e registrando-o no cache de inferência do verificador de tipos. Ao restaurar o contexto local enquanto a entrada do cache persiste e enviar uma declaração opaca com a variável não vinculada, o kernel pode inferir o tipo armazenado em cache e admitir uma constante opaca do tipo False, a partir da qual qualquer proposição se segue. Isso ocorre durante caminhos verificados comuns no nível máximo de verificação do kernel, sem a necessidade de axiomas ou conversões inseguras.

Recomendações Atualize para a versão 4.32.2.