- Verificação formal (formal verification) é um método de provar matematicamente que o código sempre satisfaz a especificação, e por muito tempo permaneceu em uma área limitada e centrada em pesquisa
- Alguns sistemas de grande porte, como o microkernel seL4, foram desenvolvidos com verificação formal, mas a alta dificuldade e o custo fizeram com que quase não fosse usada na indústria
- Recentemente, ferramentas de assistência à programação baseadas em LLM passaram a mostrar resultados não só no código de implementação, mas também na escrita de scripts de prova em várias linguagens, levantando a possibilidade de mudar drasticamente a estrutura de custos da verificação
- Se a IA puder automatizar, junto com a geração de código, até mesmo a prova de corretude, isso pode levar a uma mudança para um modelo de desenvolvimento mais confiável do que a revisão humana de código
- A automação da verificação formal é uma tecnologia central para garantir a confiabilidade de software na era da IA, e a difusão em larga escala tende a depender mais de uma mudança cultural do que de limites técnicos
O estado atual e os limites da verificação formal
- Linguagens e ferramentas orientadas a provas como Rocq, Isabelle, Lean, F*, Agda permitem provar matematicamente que o código satisfaz a especificação
- O kernel do sistema operacional seL4, o compilador C CompCert e a pilha de protocolos criptográficos Project Everest são casos representativos
- No entanto, na indústria a verificação formal quase não é usada
- No caso do seL4, verificar 8.700 linhas de código C exigiu 20 pessoa-anos e 200 mil linhas de código Isabelle
- Para cada linha de implementação, foram necessárias 23 linhas de prova e meio dia de trabalho humano
- Estima-se que existam apenas algumas centenas de especialistas no mundo capazes de escrever esse tipo de prova
- Do ponto de vista econômico, na maioria dos sistemas o custo da verificação é maior do que o prejuízo causado por bugs, por isso sua utilidade prática era baixa
Como a IA muda a economia da verificação formal
- Recentemente, assistentes de programação baseados em LLM passaram a mostrar resultados não só no código de implementação, mas também na escrita de scripts de prova
- Nature, Galois e arXiv, entre outros, relataram casos em que LLMs geraram provas em várias linguagens
- Hoje ainda é necessária a orientação de especialistas, mas espera-se que a automação completa seja possível dentro de alguns anos
- Se o custo da verificação cair drasticamente, será possível aplicar verificação formal a uma parcela muito maior do software
- Ao mesmo tempo, o código gerado por IA precisa de garantias de confiabilidade via verificação formal, em vez de revisão humana
- Se a IA puder provar por conta própria a correção do código, isso poderá torná-lo preferível ao código escrito manualmente
A complementaridade entre LLMs e verificação de provas
- Quando um LLM escreve scripts de prova, mesmo que gere conteúdo falso (alucinação), o proof checker rejeita isso
- O checker é composto por uma pequena base de código já verificada, o que torna difícil aceitar uma prova incorreta
- Assim, a rigorosidade da verificação formal compensa a incerteza dos LLMs
- Essa combinação funciona como um caminho seguro de automação para garantir a confiabilidade do código gerado por IA
Novo desafio: a precisão na definição da especificação
- Mesmo em um ambiente de verificação automatizada, definir corretamente a especificação (specification) continua sendo a tarefa central
- É preciso confirmar se a propriedade provada realmente corresponde à propriedade que o desenvolvedor pretendia
- Escrever especificações ainda exige conhecimento especializado e reflexão cuidadosa, mas é muito mais simples e rápido do que produzir provas manualmente
- A IA também pode ajudar na tradução de especificações entre linguagem natural e linguagem formal
- Ainda assim, existe risco de perda de significado, embora isso seja considerado administrável
Perspectiva de mudança na forma de desenvolver software
- Os desenvolvedores podem passar a descrever as propriedades desejadas do código em especificações declarativas, enquanto a IA gera implementação e prova em conjunto
- Nesse caso, o desenvolvedor não precisará revisar diretamente o código gerado pela IA, podendo usá-lo com base em confiança, como o código de máquina de um compilador
- Em resumo, esperam-se as três mudanças a seguir
- Queda acentuada no custo da verificação formal
- Aumento da demanda por verificação para garantir a confiabilidade de código gerado por IA
- A precisão da verificação formal complementando a natureza probabilística dos LLMs
- Se esses fatores se combinarem, a verificação formal tem grande chance de se consolidar como uma tecnologia mainstream da engenharia de software
- No futuro, o principal fator limitante provavelmente será menos a tecnologia e mais a velocidade com que a cultura de desenvolvimento aceitará essa mudança
1 comentários
Comentários do Hacker News
Acho que a verificação formal (formal verification) mostra seu verdadeiro valor em áreas em que a implementação é muito mais complexa do que a especificação
Por exemplo, em lugares como otimizações em nível de bit em implementações criptográficas ou etapas de otimização de compiladores
Mas, como o código escrito pela maioria dos desenvolvedores (ou pela IA) já é próximo da especificação graças às linguagens de alto nível, não vejo um ganho tão grande com verificação formal
Também tenho dúvidas se escrever uma especificação separada realmente ficaria mais legível
Mesmo hoje, vários frameworks e bibliotecas já abstraem os detalhes de implementação
A verificação formal pode oferecer garantias mais fortes, mas a maioria das pessoas não quer esse nível de garantia, e acho que a IA também não vai criar essa necessidade do nada
Algumas pessoas preveem que a IA vai automatizar completamente a verificação formal, mas acho que há um problema nessa lógica
Se a IA puder provar software automaticamente, nem haveria tanta necessidade de verificar software escrito por humanos
Afinal, ela própria poderia conceber ideias, implementá-las e decidir o nível de verificação
No fim, é bem possível que a programação e a verificação feitas por humanos desapareçam
Na prática, é possível que humanos projetem assistentes de prova, mas verificar programas de grande escala com eles é muito mais difícil
Portanto, se uma IA dessas surgir, ela provavelmente também conseguiria criar novos assistentes de prova por conta própria
Claro que esse tipo de imaginação está mais para o campo da ficção científica e, sem saber claramente o que a IA vai tornar mais fácil ou mais difícil, previsões assim têm pouco valor
Link para a discussão relacionada
Isso parece ser o ponto de virada em que a humanidade entra numa fase completamente diferente
Para obter resultados úteis com agentes de programação (Claude Code, Codex CLI etc.), o ponto central é montar bem um ambiente em que eles possam executar e verificar o código que escreveram
Linguagens fáceis de executar, como Python, são as mais adequadas, e para HTML+JS é preciso usar ferramentas como Playwright
O passo seguinte são suítes de testes automatizadas, e depois ferramentas de qualidade como formatadores de código, linters e fuzzers
Debuggers também são bons, mas há o problema de serem interativos e difíceis para agentes lidarem
Também considero que ferramentas de verificação formal fazem parte desse espectro — porque os modelos atuais também lidam bem com linguagens de programação especializadas
Se você sente que agentes de programação não são muito úteis, há uma boa chance de faltar ambiente de execução e de testes
Pegando Haskell como exemplo, se compila, quase sempre funciona direito
Se essa característica é útil para humanos, deve ser igualmente útil para LLMs
Em especial, property tests combinam bem com LLMs — porque conseguem cobrir uma área ampla de erros com poucos testes
Vendo tentativas na comunidade matemática de usar LLMs para melhorar código em Lean, parece bem plausível também desenvolver software aproveitando sistemas de tipos mais poderosos
Depuração não é sequencial, e os momentos de causa e efeito ficam misturados
No passado, tentei usar o ChatGPT ao caçar um bug multithread com gdb, mas ele só repetia sugestões simples de adicionar prints
No fim, senti de novo que essa é uma área que exige experiência e intuição
Não faz sentido mandar um engenheiro júnior trabalhar sem debugger ou test runner
No fim, parece que vamos precisar de mais recursos computacionais
O Claude implementa, e Codex e Gemini revisam
Esse método custa caro, mas foi a forma mais confiável que encontrei para reduzir viés próprio (self-bias) e melhorar a qualidade do código
Ferramentas de análise estática provavelmente ajudam mais um pouco, mas sinto que simplesmente adicionar mais ferramentas não basta
Quando o processo de verificação for automatizado, a parte realmente difícil passa a ser definir com precisão a especificação (specification)
Escrever a especificação é muito mais rápido e fácil do que fazer a prova em si, mas ainda exige especialização e cuidado
No passado, a prova formal não se espalhou só por ser difícil, mas também porque o modelo waterfall desapareceu e o desenvolvimento ágil virou dominante
Em vez de escrever longas especificações, a evolução foi para iterar rapidamente conforme as necessidades dos usuários
Acho que chegou a hora de aprender OCaml
Muitos assistentes de prova e sistemas de verificação conseguem gerar código OCaml, e ADA/Spark também vale considerar
De um jeito ou de outro, a engenharia de software vai mudar na era da IA, mas precisamos produzir software de qualidade mais alta do que hoje
A verificação formal certamente vai ajudar nesse objetivo
Ainda está inacabado, mas compartilho meu projeto experimental
Num mundo com poucos textos centrados em código, pode servir de referência para quem estiver procurando uma ideia interessante de hackathon
Link do projeto py-mcmas
LLMs tendem a resolver bem problemas fáceis de verificar
Por isso, eu divido a resolução em três etapas
1️⃣ primeiro escrevo um programa com a condição de sucesso
2️⃣ depois faço esse programa verificar o problema original
3️⃣ e por fim eu mesmo confiro
Essa abordagem já é antiga para mim, mas agora modelos como Opus ou GPT-5.2 conseguem fazer isso bem até em modo autônomo
Post de blog relacionado
Em áreas em que a verificação demora muito, isso pode até aumentar a carga de validação humana
Pode surgir a pergunta: “quem verifica o programa de verificação?”
Se o LLM também escrever isso, pode parecer uma torre infinita de tartarugas (turtles all the way down)
O difícil é o processo de criar a prova
Claro, há exceções em proposições complexas, mas isso ajuda muito a reduzir bugs
Mesmo que a verificação formal se popularize, não acho que todo mundo vá passar a usar Lean ou Isabelle
O mais provável é que ela se espalhe de uma forma em que a IA se integre naturalmente ao workflow existente
Por exemplo, verificação de propriedades no CI, ou um botão na IDE como “provar o invariante deste módulo”
A maioria dos engenheiros provavelmente nem vai precisar ver scripts de prova diretamente
O realmente difícil não é o LLM gerar provas, mas fazer a organização investir em escrever especificações e modelos
Se a IA facilitar propor e revisar especificações, a verificação vai se firmar como uma ferramenta natural de refatoração, como testes ou linters
Há quem reclame que o GPT‑5.2 nem consegue contar direito quantos r existem em “garlic”
Se realmente precisar, basta pedir ao LLM que escreva e execute um script em Python
Está correto, mas é só um detalhe de implementação da tokenização e quase não tem relação com utilidade real
Quase nunca há motivo para usar um LLM para contar letras dentro de palavras