Qué liberó Mistral
El 2 de julio de 2026 el laboratorio francés de IA Mistral publicó Leanstral 1.5 bajo licencia Apache-2.0, con pesos abiertos en Hugging Face y un endpoint de API gratuito. Según el propio anuncio de Mistral, es un modelo de mezcla de expertos, 119B de parámetros totales con unos 6B activos y un contexto de 256k tokens, especializado en demostración formal de teoremas en Lean 4 y autoformalización. En términos llanos, probar en Lean 4 significa convertir una afirmación sobre su software en un enunciado que una máquina comprueba línea a línea, de modo que la corrección se demuestra en vez de suponerse.
Los resultados de referencia rozan la saturación: 100 por ciento en los conjuntos de validación y prueba de miniF2F, 587 de 672 problemas de PutnamBench resueltos, 87 por ciento en FATE-H y 34 por ciento en FATE-X, con un fuerte escalado en tiempo de cómputo, de 44 problemas con poco presupuesto hasta 587 con mucho. Más revelador para un propietario, en pruebas el modelo descubrió 5 errores desconocidos en 57 repositorios de código, incluido un desbordamiento crítico en una biblioteca de decodificación zigzag que los tests convencionales suelen pasar por alto.
Escribir código era la mitad fácil
Lograr que una IA escriba código está en gran parte resuelto. Probar que ese código es correcto no lo está, y esa es la mitad que importa para todo lo que no puede permitirse que salga mal. A medida que los modelos generan más de su software, el volumen de código supera la capacidad humana de revisión, y la capa de verificación se convierte en silencio en el cuello de botella y en la garantía real.
Por eso un motor de pruebas como Leanstral pesa más que otro generador de código. Para el software crítico y regulado, la corrección demostrable pasa de lujo académico a un requisito realista de contratación, donde una prueba demostrada vale lo que ninguna batería de tests aprobados puede igualar. El propietario que puede acreditar que un componente está probado, y no solo testado, negocia desde una posición más firme ante reguladores, aseguradoras y clientes.
Poseer el verificador
La cuestión de soberanía aquí no es otro chatbot. Es el verificador. Como Leanstral se distribuye como pesos abiertos europeos bajo Apache-2.0, usted puede ejecutar la capa de comprobación en casa, inspeccionar exactamente qué hace y conservarla, en lugar de llamar a una API estadounidense y confiar en una caja negra que ni ve ni retiene.
Así la capa de confianza de su cadena de suministro de software sigue siendo auditable y bajo su control. Cuando las máquinas escriben el código, la pregunta decisiva es quién posee la máquina que comprueba la máquina. Un motor de pruebas que usted mismo ejecuta responde a esa pregunta a su favor, y lo hace sin obligarle a ceder su código más sensible a un servicio ajeno.
Leer a continuación: Su renovación de Microsoft es una palanca · La nube soberana ahora viene con nota
