Leanstral e o contrato do coding agent: quando a IA encosta num verificador formal

O lançamento mais relevante da Mistral neste ciclo não é o Mistral Small 4. É o Leanstral. Small 4 consolida um vetor já perseguido pela indústria inteira: unificar raciocínio, multimodalidade e coding num modelo open-weight mais eficiente. Leanstral mexe em algo arquitetonicamente mais profundo para quem põe LLMs dentro de pipelines de software — ele redefine o contrato entre agente e ambiente. O entregável deixa de ser “um patch plausível” e passa a ser “um artefato que atravessa um verificador formal sem quebrar”.

Este artigo explora por que esse reposicionamento importa, o que o Leanstral traz de concreto, e como ele sinaliza um deslocamento mais amplo na engenharia de coding agents: a emergência de ambientes verificáveis como peça central do loop de produção, e não como auditoria esporádica.

O contexto: Lean 4 já não é mais curiosidade acadêmica

Lean se define como linguagem de programação e proof assistant voltado a código formalmente verificado. O ecossistema articula explicitamente três vetores de aplicação: software, hardware e theorem proving assistido por IA. Três fatos concretos sustentam essa maturação:

Mathlib, a biblioteca matemática do ecossistema, já passou de 2 milhões de linhas, com linters, CI e infraestrutura de manutenção típica de engenharia de software séria.
O projeto de formalização do Último Teorema de Fermat está ativo em Lean, criando um repositório formal longo, cheio de contexto acumulado e com PRs contínuos — exatamente o tipo de ambiente onde tooling de prova deixa de ser demo e passa a ter custo operacional real.
A AWS publicou no AWS Open Source Blog a experiência de uso de Lean no Cedar (linguagem de políticas de autorização): modelo mais compacto, prova interativa, testes diferenciais em escala e feedback rápido o bastante para ficar próximo do ciclo normal de desenvolvimento. A Amazon Science descreve o efeito: quando especificação, prova e CI entram no fluxo normal, sobem linhas verificadas, bugs encontrados e velocidade de correção, porque o verificador deixa de ser auditoria rara e vira parte do loop de engenharia.

Essa base é o que torna o Leanstral possível. Sem um ecossistema formal com massa crítica, um modelo treinado para proof engineering teria ambiente ralo demais para demonstrar valor.

O que o Leanstral é tecnicamente

O Leanstral foi anunciado em 16 de março de 2026 como o primeiro code agent open-source desenhado especificamente para Lean 4. Os parâmetros principais, segundo a documentação oficial e o anúncio da Mistral:

Pesos distribuídos sob licença Apache 2.0.
Janela de contexto de 256k tokens.
Arquitetura esparsa: 119B parâmetros totais, aproximadamente 6B ativos por token.
Endpoint gratuito disponível em Mistral Labs.
Alvo explícito: proof engineering em repositórios formais reais, não problemas isolados de olimpíada.

O ponto arquitetural relevante não é o tamanho — é o alvo. Um modelo esparso da ordem de 119B/6B ativos é um vetor de custo-eficiência conhecido. O diferencial é a seleção do domínio: trabalho dentro de repositórios Lean com estado acumulado, históricos de PR e dependências sobre Mathlib.

FLTEval: um benchmark colado ao trabalho real

A avaliação proposta pela Mistral segue a mesma lógica arquitetural. Em vez de benchmark sintético, o FLTEval mede duas coisas em pull requests do projeto FLT:

Completar provas formais pendentes.
Definir novos conceitos matemáticos que serão consumidos por outras partes da formalização.

Isso importa porque FLT é um repositório longo, com contexto profundo, onde o custo de navegação, leitura de dependências e manutenção de estado conceitual é parte não trivial do trabalho. Benchmarks que isolam tarefas de sua cadeia de dependências inflacionam performance aparente. O FLTEval força o modelo a operar sobre a estrutura real de um projeto formal.

Os números publicados

A Mistral publicou resultados que comparam o Leanstral a modelos gerais de fronteira no FLTEval:

Modelo	Métrica	Score	Custo
Leanstral	pass@2	26,3	US$ 36
Sonnet 4.6	pass@2	23,7	US$ 549
Leanstral	pass@16	31,9	US$ 290
Opus 4.6	pass@16	39,6	US$ 1.650

Opus 4.6 ainda supera em qualidade bruta, mas com custo cerca de 5,7x maior que o Leanstral no setup pass@16 mostrado. Como sempre, benchmark de fornecedor deve ser lido com ceticismo. O ponto arquitetural, entretanto, se mantém: quando o ambiente contém um verificador duro no final do loop (a prova fecha ou não fecha), pass@N deixa de ser ginástica estatística e passa a ser estratégia operacional legítima. Multiplicar tentativas baratas contra um árbitro determinístico é economicamente viável.

A demo operacional: uma quebra real no Lean 4.29.0-rc6

Dos exemplos apresentados, o mais representativo não é o gráfico comparativo, mas um caso de regressão técnica: o Leanstral analisou uma quebra real no Lean 4.29.0-rc6, reproduziu a falha, isolou a causa e propôs uma correção que trocava def por abbrev para restaurar a igualdade definicional exigida pela tática rw.

Esse tipo de diagnóstico requer três capacidades simultâneas que separam um agente de código de um autocomplete caro:

Compreensão semântica da linguagem (diferença entre def e abbrev afeta redução definicional).
Modelagem do comportamento de ferramentas internas (como rw resolve igualdades).
Noção explícita do que precisa ser verdadeiro para a prova fechar.

Nenhum desses três eixos sobrevive a um modelo que apenas completa tokens. São propriedades de um sistema treinado para operar no ambiente que o verificador impõe.

O problema que o Leanstral ilumina fora de Lean

O gargalo que o Leanstral ataca não é específico de proof assistants. Em qualquer codebase de produção séria, a dificuldade não está em produzir código — está em fechar o ciclo de confiança antes do merge. Quando o patch toca em autenticação, política de acesso, regra de faturamento, migração de schema, permissão IAM ou rollback de deploy, ninguém aprova no escuro um diff “que parece certo”. A velocidade morre no gargalo de revisão.

Em Lean, esse problema aparece sem disfarce. A prova fecha ou não fecha. O verificador não é impressionado por patch elegante ou por comentário persuasivo. Esse reducionismo do sinal de confiança a um checker determinístico é o que torna o ambiente formal particularmente adequado a coding agents.

O padrão generalizável: agente + verificador forte

A implicação técnica não é “adote Lean 4 no monorepo”. É outra: o coding agent útil em produção é aquele que trabalha encostado num verificador forte. Esse verificador pode assumir várias formas, a depender do domínio:

Compilador ou typechecker estrito (Rust, TypeScript strict, Haskell)
Suíte de contrato (property-based testing, contratos de API)
Checker de política (Cedar, OPA, SPL)
Validador de migração de schema
terraform plan com drift detection
Model checker (TLA+, Alloy)
Proof assistant (Lean, Coq, Isabelle)

O que une essas peças é uma propriedade: produzem um sinal binário ou altamente estruturado sobre a correção de um artefato proposto pelo agente, sem depender de revisão humana subjetiva. Esse sinal é o que permite ao agente iterar com alto throughput sem colapsar o tempo do revisor humano.

A Amazon Science documenta o efeito composto dessa integração: quando spec, prova e CI entram no fluxo normal de desenvolvimento, sobem três métricas simultaneamente — linhas verificadas, bugs encontrados e velocidade de correção.

Os trade-offs reais

A leitura honesta dessa direção exige reconhecer limitações concretas:

Prova formal não corrige requisito mal escrito. Se a especificação está errada, o que se obtém é uma prova impecável da coisa errada. O valor da verificação é condicionado à qualidade da spec.
Lean tem curva de aprendizado séria. A própria AWS documenta a adaptação cognitiva exigida pelo termination checker e por modelos de dados menos confortáveis que os de linguagens de produção convencionais.
Custo de manutenção de repositórios formais não é trivial. Mathlib só escala porque tem infraestrutura e comunidade dedicadas.

O Leanstral não remove esses custos. Ele torna mais viável amortizá-los, transferindo parte do trabalho repetitivo de proof engineering para um agente especializado.

O reposicionamento do mercado

O ciclo anterior de coding agents privilegiou capacidades horizontais: abrir arquivos, chamar ferramentas, executar comandos, gerar testes. Essas capacidades continuam relevantes, mas não são mais suficientes como eixo de diferenciação. O Leanstral aponta para um segundo eixo: agentes cujo trabalho pode ser rejeitado por um sistema independente com rigor de máquina.

Essa é uma mudança de contrato técnico. O agente deixa de ser avaliado pela plausibilidade do output e passa a ser avaliado por uma função externa de correção. Em domínios onde essa função existe ou pode ser construída, a adoção de coding agents deixa de depender de processo humano intensivo de revisão e passa a operar em regime de throughput.