Patrick Hulin

**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.