Temos prova por automação agora
A verificação formal de software, há muito vista como cara e especializada demais, está sendo remodelada por grandes modelos de linguagem que agora conseguem gerar e automatizar muitas provas dentro de sistemas como o Lean. Comentadores argumentam que isso pode tornar viável, para mais domínios, código de alta garantia e até assembly verificado, especialmente em casos críticos de segurança, mas enfatizam que escrever boas especificações e abstrações continua sendo a parte difícil e que métodos formais ainda podem provar o comportamento “errado” como correto se a especificação estiver defeituosa. Há um debate ativo sobre como tipos dependentes e funções totais escalam na manutenção de sistemas reais e se a verificação guiada por LLMs mudará de fato as práticas de engenharia de software mainstream ou permanecerá focada em casos críticos de borda.
LLMs + Automação de Provas
- Muitos veem LLMs + provadores de teoremas (Lean, sistemas ao estilo HOL, etc.) como uma mudança de patamar: agora eles conseguem descarregar grandes partes de provas que antes levavam dias ou semanas.
- Irrelevância de provas, somada à automação, pode tornar sistemas ricos de tipos dependentes mais práticos, reduzindo o esforço de “engenharia de provas”, embora boa decomposição de problemas e abstrações continuem sendo críticas.
- Alguns descrevem experimentos bem-sucedidos em que LLMs recriaram provas formais de vários dias em minutos, sugerindo que projetos de verificação antes “insanos” (kernels, grandes teoremas) se tornam plausíveis como esforços solo.
Especificações como o Gargalo
- Vários argumentam que a parte mais difícil não é provar correção, mas defini-la: software do mundo real frequentemente não tem comportamento preciso para casos de borda (falhas de rede, backups, serializadores, etc.).
- Escrever especificações formais pode exceder o comprimento e a complexidade do código; bugs em especificações se traduzem diretamente em sistemas “verificados”, porém errados.
- Especificações parciais (por exemplo, ida e volta, compactar/descompactar como inversos, “nunca executa código arbitrário”) ainda são vistas como muito valiosas.
Tipos Dependentes, Manutenção e Design de Linguagens
- Uma corrente afirma que tipos dependentes e funções totais não escalam para sistemas grandes: adicionar uma nova propriedade pode exigir encaminhar novos invariantes por muitos tipos e provas.
- Contraponto: isso é análogo a manter a correção em qualquer sistema grande; boa estruturação (separar preocupações, usar tipos opacos, pequenos núcleos confiáveis) mitiga a dor.
- Futuras linguagens que integrem verificação ao sistema de tipos são vistas como promissoras, mas muitos esperam que a maioria dos programas apenas verifique partes críticas, não sistemas inteiros.
Segurança, Cripto e Assembly Verificado
- Blockchains e cripto são destacados como candidatos ideais: adversários fortes, histórico de métodos formais e interesse em assembly e compiladores verificados.
- À medida que encontrar explorações fica mais barato (inclusive via IA), alguns argumentam que a verificação formal se torna economicamente mais atrativa; outros acham que as organizações vão parar em uma busca automatizada por bugs “boa o suficiente”.
Comportamento, Alinhamento e Limites dos LLMs
- LLMs frequentemente evitam trabalho pesado de prova a menos que sejam fortemente instruídos, preferem soluções superficiais e podem ignorar bibliotecas poderosas se não forem coagidos.
- Eles também podem implementar um recurso incorretamente e depois gerar testes/especificações que “provem” o comportamento errado, então a revisão humana das especificações continua essencial.
- Entusiastas veem métodos formais + LLMs como transformadores; céticos alertam que isso principalmente desloca a dificuldade para a especificação em nível mais alto e não substituirá testes nem o julgamento humano.