Leanstral: agente open source para engenharia confiável de código e provas formais

• O primeiro agente de código open source projetado para Lean 4, com o objetivo de automatizar provas formais (formal proof) e reduzir a carga de verificação humana
• Publica os pesos do modelo sob a licença Apache 2.0 e está disponível para uso imediato no ambiente Mistral Vibe e por meio de um endpoint de API gratuito
• Usa uma arquitetura esparsa com 6B de parâmetros ativos para alcançar eficiência e redução de custos, além de oferecer suporte a integrações MCP como lean-lsp-mcp
• No benchmark FLTEval, obteve pontuação superior à de grandes modelos open source como Qwen3.5, GLM5 e Kimi-K2.5, e mostrou desempenho semelhante ao Claude Sonnet com custo mais de 15 vezes menor
• Apresenta uma nova abordagem que combina automação de provas formais e aumento da confiabilidade de código, com potencial de uso tanto em matemática de pesquisa quanto no desenvolvimento de software de missão crítica

---

Visão geral do Leanstral

• Leanstral é o primeiro agente de código open source para Lean 4, operando em um ambiente de assistente de provas (proof assistant)
  • Lean 4 pode expressar objetos matemáticos complexos (ex.: espaços perfectoid) e especificações de software
  • Ao contrário de sistemas de prova existentes, que se concentram em wrappers de modelos gerais ou em problemas isolados, o Leanstral foi treinado para operar com eficiência em repositórios formais realistas (formal repositories)
• Adota uma arquitetura esparsa com 6B de parâmetros ativos, combinando inferência paralela (parallel inference) com os recursos de verificação do Lean
• Oferece suporte à integração MCP, sendo compatível com protocolos amplamente usados, como o lean-lsp-mcp

Lançamento e acessibilidade

• Publica os pesos do modelo sob a licença Apache 2.0 e o oferece no modo agente dentro do Mistral Vibe
• Está acessível a qualquer pessoa por meio do endpoint de API gratuito (labs-leanstral-2603), e o feedback dos usuários será usado para melhorar os próximos modelos
• Também publica o relatório técnico e a ferramenta de avaliação FLTEval, medindo o desempenho real em engenharia de provas para além das avaliações centradas apenas em matemática

Avaliação de desempenho (Evaluation)

• Avaliado com base na capacidade de concluir todas as provas formais e definir novos conceitos matemáticos em unidades de Pull Request do projeto FLT
• Comparativos: Claude Opus 4.6, Sonnet 4.6, Haiku 4.5, Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B

Leanstral vs. modelos open source

• Leanstral-120B-A6B registrou 26.3 pontos (pass@2), acima de GLM5 (16.6) e Kimi-K2.5 (20.1)
• Enquanto o Qwen3.5 obteve 25.4 pontos em 4 execuções (pass@4), o Leanstral alcançou uma pontuação maior com metade das execuções
• No mesmo nível de custo, escala linearmente até 29.3 pontos (pass@4)

Leanstral vs. família Claude

• Mostra vantagem de 2.6 pontos sobre o Sonnet (26.3 vs 23.7), com custo de execução de $36 vs $549, mais de 15 vezes menor
• Em pass@16, registrou 31.9 pontos, 8 pontos acima do Sonnet
• O Claude Opus 4.6, de melhor desempenho, marcou 39.6 pontos, mas com custo de $1,650, 92 vezes maior que o Leanstral
• Todos os benchmarks foram executados no ambiente Mistral Vibe sem modificações

modelo	custo($)	pontuação
Haiku	184	23.0
Sonnet	549	23.7
Opus	1,650	39.6
Leanstral	18	21.9
Leanstral pass@2	36	26.3
Leanstral pass@4	72	29.3
Leanstral pass@8	145	31.0
Leanstral pass@16	290	31.9

Estudos de caso (Case Studies)

Adaptação a mudanças de versão do Lean

• Recebeu como entrada uma pergunta do StackExchange sobre um erro relacionado a alias de tipo ocorrido no Lean 4.29.0-rc6
• O Leanstral reproduziu o ambiente do problema e diagnosticou com precisão uma questão de igualdade definicional (definitional equality)
• Sugeriu usar abbrev no lugar de def, corrigindo o funcionamento normal da tática rw (tactic)
• Explicou claramente ao usuário a causa do problema e o motivo da solução

Raciocínio e transformação de programas

• Converteu definições de programa em Rocq para Lean, inclusive implementando notação personalizada definida pelo usuário
• Como exemplo, provou que o comando plus2 executa a ação de adicionar 2 à variável X
• Completou e provou o teorema (theorem) em Lean usando apenas a especificação fornecida em Rocq

Como usar

• Integração com Mistral Vibe: disponível imediatamente com o comando /leanstall
• Labs API: acesso gratuito ou de baixo custo
• Download do modelo: pode ser executado diretamente sob a licença Apache 2.0

Significado

• Leanstral é a primeira tentativa open source de combinar geração de código e automação de provas formais
• Aponta potencial de uso em matemática de pesquisa, desenvolvimento de software verificável e projeto de sistemas de alta confiabilidade
• É avaliado como uma nova infraestrutura de verificação de código que reúne eficiência de custo e abertura

[GN⁺]

Comentários do Hacker News

• É interessante que as pessoas estejam começando a reconhecer o padrão de especificar para o agente o comportamento desejado e então fazer com que ele escreva o código de acordo com essa especificação
  Seja com TDD, ferramentas de verificação ou qualquer outro método, com o tempo essas suítes de verificação acabam se acumulando como um repositório de documentação executável que mostra “como isso deve funcionar”
  Essa abordagem é muito mais poderosa do que uma especificação simples em Markdown, porque registra no código não a intenção, mas o comportamento detalhado
  À medida que o software fica mais complexo, esse tipo de tradição oral de “pergunta pro Jim” tem limites

  • Não parece uma diferença tão grande. No fim, código também é apenas outra forma de expressar a informação que estaria em um arquivo .md
    Minúcia e contexto se perdem conforme a resolução muda
    Concordo com TDD e com desenvolvimento centrado em verificação, mas escrever isso em código não é o objetivo final
    Já existem milhões de linhas de testes, então o realista é evoluir a partir deles
  • Acho que foi só com a chegada da IA que a realidade que o TDD sonhava se tornou possível
  • Essa abordagem é interessante, mas o post do blog foi confuso
    Fiquei curioso sobre que ajuda o Lean de fato oferece.
    Por exemplo, seria algo como provar uma máquina de estados em Lean e depois portar isso para Dart?
    Como não conheço bem Lean, não consigo ter noção se isso é uma abordagem realista

• Como também foi mencionado recentemente no podcast de Jack Clark (cofundador da Anthropic) com Ezra Klein, há muita discussão de que alinhamento de modelos (alignment) é algo relativo e de que diversidade é importante
  Há opiniões de que os modelos da Mistral ficam atrás de outros modelos de fronteira, mas experimentar diferentes técnicas de alinhamento e diferentes empresas é importante para o ecossistema

  • No fim, acho que o tempo vai resolver isso

• O caso de sucesso real lembra o Red Green TDD do Simon Willison
  Foi marcante o processo em que o Leanstral criou código de teste para reproduzir um ambiente de falha e encontrou um problema de igualdade definicional (definitional equality)

  • Se o agente escrever os próprios testes, será que a garantia de correção fica maior do que quando código e testes são escritos separadamente?
  • No fim das contas, TDD é como engenharia de prompt. É o processo de dar um objetivo claro ao agente

• Esse modelo foi treinado para tarefas específicas, mas tem desempenho inferior ao Opus
  O Opus custa 6 vezes mais, mas parece valer isso

  • A ideia é boa, mas no fim qualidade vem antes de confiabilidade
    Entendo uma startup europeia com pouco capital mirar esse nicho, mas parece difícil que isso leve a grande receita
  • A confiabilidade dos benchmarks é meio ambígua, mas olhando os resultados de pass@2 ou pass@3 a impressão muda
    Acho que seria mais interessante comparar com modelos como o Codex
  • O modelo é open source, então pode rodar localmente. Isso não é um ponto bem importante?

• Gosto do conceito de “código confiável”
  Mas o critério de comparação é confuso. Enfatizam que é mais barato que o Haiku, mas o próprio Haiku é fraco nessa tarefa, e o Leanstral é ainda mais fraco
  Se o objetivo é precisão, não entendo por que “barato, mas mais ou menos” seria importante
  Ainda assim, como o Opus também não é perfeito, talvez ao aumentar a escala possa gerar resultados melhores

  • Pelos gráficos, o desempenho melhora conforme se aumenta o número de passagens
    Em 2 tentativas ele é melhor que Haiku e Sonnet, e em 16 tentativas se aproxima do Opus, mantendo boa eficiência de custo
  • Na verdade é simples — basta pedir no prompt “somente saídas confiáveis”

• Para quem não conhece Lean, fico curioso se isso tem valor direto
  Ele adiciona provas automaticamente a código em linguagens como Go, ou a ideia é apenas apoiar a diversidade de modelos abertos?

  • Provavelmente a estrutura é que o agente gera uma especificação em Lean4 e avalia o software com base nessa especificação
    Mas no fim a própria especificação em Lean4 vira um artefato de software
    Então voltamos ao problema de verificar se essa especificação está correta — no fim, ainda é necessária revisão humana

• Eu já vinha prevendo essa tendência há algumas semanas, então fico feliz de ver que estava certo
  Na era dos LLMs, parece que a amigabilidade do código para humanos será menos importante do que capacidade de prova e eficiência de tokens
  Ao combinar Lean e Rust, talvez possamos chegar a um mundo em que “só código provado compila”
  Resumi a discussão em um comentário anterior

  • Mas nenhum sistema de prova garante uma “prova correta”
    Ele apenas garante que ela é logicamente válida (valid)
    Entender completamente o que uma prova está provando é tão difícil quanto entender um programa, embora esse processo tenha a vantagem de aprofundar o raciocínio

• Foi bom ver que “open source” não ficou só no discurso e que os pesos sob licença Apache-2.0 foram realmente publicados

  • Mas, pelos padrões da comunidade, se o modelo não pode ser reproduzido, então ele é apenas open weights, não “open source”

• Segundo as notícias oficiais da Mistral,
  Claude Opus tem pontuação 39.6 a um custo de 1.650 dólares,
  Leanstral pass@8 tem 31.0 por 145 dólares, e pass@16 tem 31.9 por 290 dólares,
  então a eficiência de desempenho por custo é bem alta