Criador do Lean diz que IA tornou verificação formal viável para o dia a dia dos devs

O gargalo não é mais gerar código, é confiar nele

Em entrevista ao podcast The Data Exchange, conduzida por Ben Lorica, Leo de Moura (criador do Lean, VP e Distinguished Scientist na AWS↳AWS20 conteúdosE-mails de verificação com AWS SES + Lambda (Node.js) e Terraform: do zero ao envioDevSecOps · out 2025Codex na AWS: chegada do agente da OpenAI à nuvem da AmazonDevSecOps · abr 2026Salesforce e AWS ampliam colaboração em IA, CRM e marketplaceDevSecOps · nov 2023Ver tudo em DevSecOps →, e Chief Architect da Lean Focused Research Organization) descreve um cenário que muda a régua de quem escreve software assistido por IA↳Inteligência artificial440 conteúdosUX e IA: Transformando Experiências Digitais com Inteligência ArtificialProduto & UX · jan 2025MCP: O que é e por que você vai ouvir falar disso em breve?AI · jul 2025IA generativa e a urgência de reconstruir nossa relação com a verdadeAI · jun 2025Ver tudo em AI →: gerar código ficou fácil, mas provar que ele está correto continua sendo o problema de verdade.

Lean é ao mesmo tempo uma linguagem de programação e um assistente de provas. Nele dá para escrever código e, junto, declarar as propriedades que esse código deveria ter, com provas matemáticas verificadas por máquina. A parte que precisa de confiança é pequena: o kernel que checa a prova. Todo o resto, LSP, autocomplete, geração de código, serve só de apoio.

Testes são ótimos para mostrar a presença de bugs, mas não a ausência deles.

Leo de Moura, criador do Lean e VP Distinguished Scientist na AWSTesting is great for showing the presence of bugs, but not their absence.

A diferença entre testar e provar

A distinção que de Moura faz entre QA tradicional e verificação formal ajuda a entender por que uma coisa não substitui a outra.

Segundo ele, as duas técnicas são complementares, não concorrentes: vale testar primeiro para ganhar confiança e entendimento do problema, e só depois partir para a prova, que cobre qualquer entrada possível em vez de só os casos pensados pelo time.

Da tradução automática ao Mathlib de 2,5 milhões de linhas

O salto que de Moura credita à IA tem nome: autoformalização, a capacidade de um modelo ler um texto (paper de matemática, ou código em qualquer linguagem) e traduzi-lo para Lean sozinho.

Se alguém tivesse me dito isso ano passado, eu diria que é ficção científica.

Leo de Moura, criador do Lean e VP Distinguished Scientist na AWSI mean, if someone had told me this last year, I would have said this is science fiction.

O exemplo que ele usa para dimensionar o salto é o Mathlib, a biblioteca matemática do Lean mantida por humanos: 2,5 milhões de linhas construídas ao longo de dez anos. Hoje já existem provas escritas por IA publicadas com 50 milhões de linhas, e a prova do Último Teorema de Fermat, escrita por um sistema da Anthropic, tem 13 milhões de linhas.

Verificando código de verdade: zlib, Rust e a SymCrypt da Microsoft

Para sair do terreno da matemática pura, de Moura cita um experimento de uma colega, Kim Morrison: ela portou a biblioteca de compressão zlib para Lean e provou formalmente que comprimir e depois descomprimir um dado sempre devolve o dado original, sem perda, para qualquer nível de compressão.

Para quem programa em Rust↳Rust7 conteúdosDesmistificando Rust: a linguagem segura e rápida que você precisa conhecerDev (Back & Front) · out 2024Como criar seu primeiro Programa em Rust com Solana PlaygroundDev (Back & Front) · mai 2026Rust no ranking: a segurança de memória perdeu a guerra corporativa?Marketing Tech · abr 2026Ver tudo em Dev (Back & Front) →, existe um caminho mais direto: a ferramenta Aeneas permite verificar código Rust usando Lean sem reescrever o projeto inteiro na linguagem. Segundo de Moura, o time de SymCrypt da Microsoft (a biblioteca criptográfica da empresa) já usa Aeneas combinado com Lean para verificar a própria biblioteca de criptografia.

A outra alternativa, mais recente e mais genérica, é pedir à IA que construa um modelo em Lean a partir de código em qualquer linguagem, sem ferramenta dedicada. O risco embutido nessa abordagem, que o próprio de Moura destaca, é que o modelo gerado pode não ser fiel ao código original, daí a adoção de testes diferenciais: rodar o programa real e o modelo em Lean lado a lado, comparando as saídas para achar discrepâncias.

O caso Claude Code: um agente achando bugs sem o dono saber Lean

O exemplo mais concreto de uso prático veio de dentro da própria Anthropic. Segundo relato de de Moura, Boris, desenvolvedor principal do Claude Code, publicou um vídeo em que pediu ao Claude para checar o próprio Claude Code em busca de bugs usando Lean.

O agente criou modelos do código, tentou provar propriedades, identificou onde a prova não fechava, isolou bugs reais e abriu pull requests, que Boris aceitou e mergeou. Boris, segundo o relato, não sabe Lean.

Em resumo: o ganho prático aqui não é o dev virar matemático, é o agente de IA usar a prova formal como detector de bug mais rigoroso do que um conjunto de testes, mesmo sem o humano entender os detalhes da prova.

Onde a confiança ainda pode quebrar

Nem tudo é só ganho automático. De Moura usa a polêmica em torno da prova das equações de Navier-Stokes, atribuída à OpenAI, para mostrar onde o processo ainda falha: a versão informal da prova, em linguagem natural, e a versão formal em Lean tinham uma divergência sutil sobre a ordem de uma derivada (quarta versus quinta), que importa para matemáticos mesmo sendo um detalhe técnico pequeno.

A causa, segundo ele, não é falha da autoformalização em si, já que o enunciado do problema tinha sido validado por especialistas antes mesmo de a IA entrar em cena, mas a falta de uma ferramenta que mantivesse a versão em linguagem natural e a versão em Lean alinhadas automaticamente. Ele cita o Verso Blueprint, ferramenta no estilo de programação literária que mistura linguagem natural, LaTeX e Lean, como o tipo de tooling que teria evitado esse descompasso.

Outro ponto que ele reforça: uma prova em Lean não é um objeto estático. Dá para refatorá-la, simplificá-la e reduzi-la, do mesmo jeito que se refatora código, sempre com o kernel confirmando que a prova continua válida depois da mudança. Grupos independentes já reduziram a prova do Último Teorema de Fermat pela metade.

Quem checa o kernel que checa tudo

Fica uma pergunta óbvia: se tudo depende do kernel do Lean, o que garante que o próprio kernel está correto? De Moura responde que o projeto não depende de confiar apenas no time dele: existem múltiplos kernels independentes, alguns já verificados formalmente, implementados em Rust, C#, Haskell e, como curiosidade, até em TeX.

Esses kernels competem entre si em velocidade e correção no arena.lean-lang.org, de forma pública: um kernel que erra é penalizado e fica visível para qualquer um conferir.

O que muda pra quem programa no Brasil

A leitura direta para quem desenvolve software no Brasil é que formal verification deixou de ser um nicho acadêmico restrito a sistemas críticos (aviônica, protocolo de segurança) para virar uma ferramenta que um time comum pode encostar via agente de IA, sem precisar aprender Lean do zero, como no caso do Claude Code.

Isso não elimina o trabalho do engenheiro, só desloca onde ele investe tempo: em vez de revisar linha a linha, o esforço vai para escrever a especificação certa (o que o código deveria garantir) e desconfiar sistematicamente se o modelo gerado pela IA é mesmo fiel ao código em produção. De Moura resume essa mudança comparando as provas a uma rede de segurança para otimizações agressivas de IA:

É quase como se as provas fossem proteções.

Leo de Moura, criador do Lean e VP Distinguished Scientist na AWSIt's almost like the proofs are guardrails.

Para projetos brasileiros que lidam com código sensível (pagamentos, criptografia, infraestrutura), o caminho descrito por de Moura, Aeneas para quem já trabalha em Rust, ou um modelo gerado por IA com testes diferenciais para outras linguagens, é hoje tecnicamente viável sem reescrever o sistema do zero. O que ainda fica em aberto, pelo próprio relato dele, é a maturidade das ferramentas para manter a especificação formal e o código real sempre sincronizados à medida que o projeto evolui.

Fonte: Hacker News