Lean es un asistente de pruebas, una herramienta de software utilizada por matemáticos y científicos de la computación para escribir y verificar pruebas lógicas complejas. En su núcleo se encuentra un 'kernel', la pieza fundamental de código que determina si una prueba es válida. Debido a que estos núcleos son críticos para la integridad de todo el sistema, cualquier error en la implementación del kernel podría permitir que una prueba incorrecta sea aceptada como verdadera. Leonardo de Moura, cofundador de Lean FRO, anunció que Lean v4.35.0 ahora se distribuye con varios núcleos nuevos para abordar la creciente eficacia de los agentes de IA en la identificación de vulnerabilidades en este tipo de software.
Leonardo de Moura es el cofundador de Lean FRO y la figura principal que anuncia estas actualizaciones de seguridad.
Una de las principales adiciones es 'con-leche', el primer núcleo para Lean escrito en Lean mismo y demostrado como consistente. La consistencia en este contexto significa que cada entorno que el kernel acepta tiene un modelo correspondiente en la teoría de conjuntos. Al utilizar un núcleo escrito en el lenguaje que debe verificar, los desarrolladores pretenden eliminar una clase de errores causados por fallos de programación en la implementación del kernel. Para mitigar aún más los riesgos provenientes del compilador o de los entornos de ejecución utilizados para construir el software, el equipo también introdujo 'con-ron'. Este núcleo fue creado utilizando IA para traducir la lógica de con-leche a Rust, que luego fue verificado mediante Aeneas, una herramienta que demuestra que el código Rust refina el algoritmo de verificación. Al verificar una prueba contra tanto con-leche como con-ron, los usuarios pueden obtener un alto nivel de protección contra errores que podrían existir en un entorno pero no en el otro.
Si bien estos núcleos verificados proporcionan una mejora significativa en la seguridad, el equipo de Lean reconoce que la escalabilidad sigue siendo un desafío. A medida que la comunidad crece y las bibliotecas como Mathlib se expanden a millones de líneas de código, el método actual de volver a verificar los desarrollos con núcleos externos puede volverse ineficiente. El equipo está explorando actualmente formatos de exportación binaria y verificación incremental para manejar desarrollos masivos, como aquellos que superan las 100 millones de líneas de código. Mientras tanto, los usuarios pueden utilizar el nuevo comando `lake check --paranoid`, que ejecuta una variante del kernel oficial construida con un asignador de memoria endurecido para convertir una posible corrupción de memoria en un aborto verificado en lugar de un error silencioso.