Leanstral: agente open source para ingeniería de código y pruebas formales confiables

• El primer agente de código open source diseñado para Lean 4, con el objetivo de automatizar las pruebas formales (formal proof) y reducir la carga de verificación humana
• Publica los pesos del modelo bajo licencia Apache 2.0 y está disponible de inmediato a través del entorno Mistral Vibe y un endpoint de API gratuito
• Usa una arquitectura dispersa con 6B parámetros activos para lograr eficiencia y reducción de costos, y admite integraciones MCP como lean-lsp-mcp
• En el benchmark FLTEval, obtuvo mejores puntajes que grandes modelos open source como Qwen3.5, GLM5 y Kimi-K2.5, y mostró un rendimiento similar a Claude Sonnet con un costo más de 15 veces menor
• Propone un nuevo enfoque que combina automatización de pruebas formales y mejora de la confiabilidad del código, con potencial de uso tanto en matemáticas de investigación como en desarrollo de software de misión crítica

---

Resumen de Leanstral

• Leanstral es el primer agente de código open source para Lean 4, y funciona dentro de un entorno de asistente de pruebas (proof assistant)
  • Lean 4 puede expresar objetos matemáticos complejos (por ejemplo, espacios perfectoid) y especificaciones de software
  • A diferencia de los sistemas de pruebas existentes, que se enfocan en wrappers de modelos generales o en problemas individuales, Leanstral fue entrenado para operar eficientemente en repositorios formales realistas (formal repositories)
• Adopta una arquitectura dispersa con 6B parámetros activos, combinando inferencia paralela (parallel inference) con las capacidades de verificación de Lean
• Admite integración con MCP, por lo que es compatible con protocolos de uso frecuente como lean-lsp-mcp

Publicación y accesibilidad

• Publica los pesos del modelo bajo licencia Apache 2.0 y se ofrece en modo agente dentro de Mistral Vibe
• Cualquiera puede acceder mediante el endpoint de API gratuito (labs-leanstral-2603), y la retroalimentación de los usuarios se aprovechará para mejorar el próximo modelo
• También se publicaron el reporte técnico y la herramienta de evaluación FLTEval, para medir el rendimiento real en ingeniería de pruebas más allá de las evaluaciones centradas en matemáticas existentes

Evaluación de rendimiento (Evaluation)

• La evaluación se basa en la capacidad de completar todas las pruebas formales y la definición de nuevos conceptos matemáticos a nivel de Pull Request del proyecto FLT
• Modelos comparados: 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 registró 26.3 puntos (pass@2), superando a GLM5 (16.6 puntos) y Kimi-K2.5 (20.1 puntos)
• Mientras que Qwen3.5 obtuvo 25.4 puntos en 4 ejecuciones (pass@4), Leanstral logró una puntuación mayor con la mitad de ejecuciones
• Escala linealmente hasta 29.3 puntos (pass@4) dentro del mismo nivel de costo

Leanstral vs. familia Claude

• Muestra una ventaja de 2.6 puntos frente a Sonnet (26.3 vs 23.7), con un costo de ejecución de $36 vs $549, más de 15 veces más barato
• En pass@16, registró 31.9 puntos, 8 puntos por encima de Sonnet
• El modelo de mayor rendimiento, Claude Opus 4.6, registró 39.6 puntos, pero con un costo de $1,650, es decir, 92 veces más alto que Leanstral
• Todos los benchmarks se ejecutaron sin modificaciones en el entorno Mistral Vibe

Modelo	Costo($)	Puntaje
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

Estudios de caso (Case Studies)

Adaptación a cambios de versión de Lean

• Se ingresó una pregunta de StackExchange sobre un error relacionado con alias de tipos ocurrido en Lean 4.29.0-rc6
• Leanstral reprodujo el entorno del problema y diagnosticó con precisión un problema de igualdad definicional (definitional equality)
• Propuso usar abbrev en lugar de def, corrigiendo así el funcionamiento normal de la táctica rw (tactic)
• Explicó con claridad al usuario la causa del problema y por qué la solución funcionaba

Razonamiento y transformación de programas

• Convirtió una definición de programa de Rocq a Lean, implementando incluso notación definida por el usuario
• Como ejemplo, probó que el comando plus2 realiza la operación de sumar 2 a la variable X
• A partir únicamente de la especificación dada en Rocq, completó y demostró el teorema (theorem) en Lean

Cómo usarlo

• Integración con Mistral Vibe: disponible de inmediato con el comando /leanstall
• Labs API: acceso gratuito o de bajo costo
• Descarga del modelo: puede ejecutarse directamente bajo licencia Apache 2.0

Significado

• Leanstral es el primer intento open source de combinar generación de código y automatización de pruebas formales
• Plantea posibilidades de uso en matemáticas de investigación, desarrollo de software verificable y diseño de sistemas de alta confiabilidad
• Se evalúa como una nueva infraestructura de verificación de código que asegura al mismo tiempo eficiencia de costos y apertura

[GN⁺]

Comentarios en Hacker News

• Es interesante que la gente por fin esté empezando a reconocer el patrón de especificar el comportamiento deseado para un agente y luego hacer que escriba código conforme a esa especificación
  Ya sea usando TDD, herramientas de verificación u otro enfoque, con el tiempo este tipo de suites de validación terminan acumulándose como un repositorio de documentación ejecutable que muestra “cómo debe comportarse”
  Este enfoque es mucho más poderoso que una especificación simple en Markdown, porque captura en código el comportamiento detallado, no solo la intención
  Mientras más complejo se vuelve el software, más límites tiene esa tradición oral de “pregúntale a Jim”

  • Siento que la diferencia no es tan grande. Al final, el código también es solo otra forma de expresar la información que iría en un archivo .md
    El nivel de detalle y el contexto se pierden al cambiar de resolución
    Estoy de acuerdo con el TDD o el desarrollo centrado en verificación, pero escribirlo en código no es el objetivo final
    Ya existen millones de líneas de tests, así que lo realista es evolucionar a partir de eso
  • Creo que con la llegada de la IA por fin se hizo posible la realidad que soñaba el TDD
  • Este enfoque me parece interesante, pero la entrada del blog me confundió
    Me pregunto en qué ayuda realmente Lean.
    Por ejemplo, ¿la idea es demostrar una máquina de estados en Lean y luego pasar eso a Dart?
    No conozco bien Lean, así que no me queda claro si este enfoque es realista

• Como también se mencionó hace poco en el pódcast de Jack Clark (cofundador de Anthropic) y Ezra Klein, hay mucha discusión sobre que la alineación de modelos (alignment) es relativa y que la diversidad importa
  Hay quienes opinan que los modelos de Mistral están por detrás de otros modelos de frontera, pero para el ecosistema es importante experimentar con distintas técnicas de alineación y distintas empresas

  • Al final creo que el tiempo lo resolverá

• El caso de éxito real me recordó al Red Green TDD de Simon Willison
  Me impresionó cómo Leanstral creó código de prueba para reproducir el entorno de fallo y encontró un problema de igualdad definicional (definitional equality)

  • Si un agente escribe sus propios tests, me pregunto si eso ofrecerá una garantía de corrección mayor que escribir el código y las pruebas por separado
  • Al final, creo que TDD es básicamente ingeniería de prompts. Es el proceso de darle un objetivo claro al agente

• Este modelo fue entrenado para una tarea específica, pero rinde peor que Opus
  Opus cuesta 6 veces más, pero parece valer la pena

  • La idea es buena, pero al final la calidad está por encima de la confianza
    Entiendo que una startup europea con poco capital apunte a este nicho, pero no parece que eso vaya a traducirse en grandes ingresos
  • La confiabilidad de los benchmarks es ambigua, pero si ves los resultados de pass@2 o pass@3, la impresión cambia
    Sería más interesante compararlo con modelos como Codex
  • El modelo es open source, así que se puede ejecutar en local. ¿No es ese un punto bastante importante?

• Me gusta el concepto de “código confiable”
  Pero el criterio de comparación me confunde. Enfatizan que es más barato que Haiku, pero Haiku de por sí es débil en esta tarea y Leanstral es aún más débil
  Si la meta es la precisión, no entiendo por qué importaría algo “barato pero flojo”
  Aun así, como Opus tampoco es perfecto, quizá al escalarlo pueda dar mejores resultados

  • En la gráfica se ve que el rendimiento mejora al aumentar el número de pass
    En 2 intentos supera a Haiku y Sonnet, y en 16 intentos se acerca a Opus mientras mantiene una alta eficiencia de costos
  • En realidad es simple: basta con pedir en el prompt “solo salidas confiables”

• Desde la perspectiva de alguien que no conoce Lean, me pregunto si esto tiene valor directo
  ¿Se trata de añadir pruebas automáticamente a código en lenguajes como Go, o simplemente de apoyar la diversidad de modelos abiertos?

  • Probablemente la estructura sea que el agente genera especificaciones en Lean4 y evalúa el software con base en esas especificaciones
    Pero al final, la propia especificación en Lean4 se convierte en un artefacto de software
    Entonces volvemos al problema de verificar si esa especificación es correcta — al final sigue haciendo falta revisión humana

• Yo ya esperaba esta tendencia desde hace unas semanas, y me alegra haber acertado
  En la era de los LLM, parece que la amabilidad del código para humanos será menos importante que su capacidad de demostración y eficiencia de tokens
  Al combinar Lean y Rust, quizá podamos llegar a un mundo donde “solo se compile código demostrado”
  Resumí una discusión relacionada en un comentario anterior

  • Aun así, ningún sistema de pruebas garantiza una “prueba correcta”
    Solo garantiza que sea lógicamente válida (valid)
    Entender completamente qué demuestra una prueba es tan difícil como entender un programa, aunque el proceso tiene la ventaja de profundizar el razonamiento

• Se agradece que cuando dicen “open source” no sea solo de palabra, sino que realmente hayan publicado los pesos con licencia Apache-2.0

  • Pero según el criterio de la comunidad, si no se puede reproducir el modelo, entonces es solo open weights, no “open source”

• Según las noticias oficiales de Mistral
  Claude Opus obtiene 39.6 con un costo de 1,650 dólares,
  Leanstral pass@8 obtiene 31.0 por 145 dólares y pass@16 obtiene 31.9 por 290 dólares,
  así que su eficiencia costo-rendimiento es bastante alta