Resumen Técnico: CSLib – La Biblioteca de Ciencias de la Computación Ágil

Planteamiento del Problema

Si bien el asistente de pruebas Lean ha logrado un éxito significativo en las matemáticas a través de Mathlib, actualmente se carece de un repositorio unificado y exhaustivo para la formalización del conocimiento de las ciencias de la computación (CC). La base actual de conocimientos de CC en Lean es limitada, lo que obstaculiza la adopción generalizada de los métodos formales en la educación, la investigación en CC y la ingeniería de sistemas verificados a gran escala. Además, el auge de la IA en la generación de código introduce nuevos riesgos: los agentes de IA podrían introducir vulnerabilidades inadvertidamente, y actores malintencionados podrían explotar la IA para encontrar fallos de seguridad. La verificación formal es la solución propuesta ante estos riesgos, pero su adopción histórica se ha visto limitada por el inmenso esfuerzo humano requerido (por ejemplo, los más de 20 años-persona necesarios para el kernel seL4). Existe una necesidad urgente de un marco que reduzca la barrera para la verificación formal, soporte la verificación de código imperativo cotidiano y proporcione la infraestructura necesaria para el razonamiento asistido por IA en las ciencias de la computación.

Metodología

CSLib propone un enfoque técnico de dos pilares para abordar estas brechas:

Pilar 1: Formalizar las Ciencias de la Computación en Lean

Este pilar tiene como objetivo construir una biblioteca coherente e integrada de conceptos de CC formalizados, distinta de, pero sinérgica con, Mathlib.

• Modelos y Lógicas: CSLib formalizará diversos modelos de computación (deterministas, no deterministas, probabilísticos, cuánticos, funcionales, online, interactivos) y notaciones de especificación (lógica temporal, lógica de Hoare, lógica de separación, lógica lineal). A diferencia de Mathlib, que se centra en la matemática pura, CSLib apunta a artefactos específicos de la CC como sistemas de transición etiquetados y bisimulaciones.
• Algoritmos y Estructuras de Datos: La biblioteca abarcará algoritmos y estructuras de datos formalmente verificados, que van desde temas estándar de pregrado (ordenamiento, grafos, tablas hash) hasta áreas avanzadas (algoritmos cuánticos, optimización matemática).
• Análisis de Complejidad: Un objetivo clave es la formalización sistemática de la complejidad algorítmica. El artículo propone una API monádica (inspirada en el monad Writer) donde las computaciones devuelven tanto un valor como un coste de tiempo. Esto trata la complejidad temporal como un efecto computacional, permitiendo que la corrección y el análisis de complejidad sean ortogonales. Aunque actualmente depende de anotaciones manuales de tick, esto sirve como un punto de partida ligero hacia un marco universal, con planes de evolucionar hacia modelos explícitos de RAM y de consultas.

Pilar 2: Infraestructura para el Razonamiento sobre Código Cotidiano

Este pilar cierra la brecha entre el razonamiento formal de Lean y los lenguajes de programación imperativos convencionales (por ejemplo, Rust, C++, Python).

• Lenguaje de Verificación Intermedio Boole (IVL): CSLib introduce Boole, un nuevo IVL inspirado en Boogie pero embebido dentro de Lean. Boole está diseñado para parecerse al pseudocódigo, soportando constructos imperativos clásicos intercalados con especificaciones de Lean (precondiciones, invariantes de bucle, aserciones).
• Pipeline de Verificación: La arquitectura implica:
  1. Transpilación: El código de lenguajes convencionales se traduce a Boole.
  2. Generación de Condiciones: El código de Boole y las especificaciones se traducen en condiciones de verificación (VC) de Lean.
  3. Automatización de Pruebas: Estas VC se resuelven mediante la automatización de Lean, incluyendo resolvedores SMT (vía Lean-SMT), "martillos" (tácticas como smt) y potencialmente probadores basados en IA.
• Principios de Diseño: El sistema prioriza una Base de Confianza (TCB) mínima al embeber Boole profundamente en Lean. Las condiciones de verificación se generan como objetivos de Lean intuitivos, lo que permite aprovechar el rico universo de definiciones establecidas en el Pilar 1.

Contribuciones Clave

1. Marco CSLib: La introducción de una biblioteca de código abierto unificada para la formalización de la CC en Lean, con el objetivo de ser el "Mathlib para las Ciencias de la Computación".
2. IVL Boole: El diseño e implementación inicial de Boole, un lenguaje intermedio que facilita la verificación de código imperativo mediante la traducción de este en teoremas verificables por Lean.
3. API Monádica de Complejidad: Un enfoque novedoso para formalizar la complejidad algorítmica dentro de Lean, permitiendo la prueba tanto de la corrección funcional como de los límites de tiempo del peor caso (por ejemplo, para MergeSort) dentro de un mismo marco.
4. Arquitectura del Pipeline de Verificación: Una visión concreta de una cadena de herramientas que conecta el código convencional con las pruebas de Lean a través de Boole, utilizando proyectos de código abierto existentes como Strata (para el embebido profundo de dialectos) y Loom (para el embebido superficial y la generación de condiciones de verificación).

Resultados y Estado Actual

El artículo presenta un libro blanco que describe la visión y el progreso inicial en lugar de un informe de resultados experimentales a gran escala completados.

• Implementación Inicial: El repositorio CSLib ya contiene formalizaciones iniciales de semántica operativa, equivalencias de programas, modelos de autómatas, lógica lineal y algoritmos básicos de búsqueda y ordenamiento.
• Prototipo de Verificación: Se ha demostrado un prototipo de generador de condiciones de verificación. Utilizando un ejemplo de bucle simple (sumar enteros), el sistema generó con éxito condiciones de verificación de Lean para invariantes de entrada, mantenimiento de bucle y aserciones. Estas condiciones fueron resueltas automáticamente usando la táctica smt, que traduce los objetivos a fórmulas SMT, las resuelve y repliega la prueba en Lean.
• Hoja de Ruta: El proyecto traza una hoja de ruta tentativa para 2026–2027, con el objetivo de cubrir la teoría y los algoritmos de nivel de pregrado para finales de 2026, y lograr la verificación de extremo a extremo de un sistema real sustancial para finales de 2027.

Significancia y Reivindicaciones

El artículo afirma que CSLib cambiará fundamentalmente el panorama de la investigación y la ingeniería de las ciencias de la computación de dos maneras principales:

1. Impacto Práctico en la Fiabilidad del Software: Al permitir la derivación composicional de sistemas fiables a partir de componentes pre-verificados y simplificar el uso de la IA en la verificación, CSLib aborda la necesidad crítica de software seguro en una era de generación de código impulsada por IA y ataques de IA. Busca hacer que la verificación formal sea lo suficientemente escalable para la adopción comercial, yendo más allá de la "penalización de costes" de los métodos tradicionales como seL4.
2. Sinergia entre Investigación e IA: CSLib sirve como una plataforma para la investigación de la CC del siglo XXI, permitiendo el descubrimiento matemáticamente fundamentado y la reutilización a gran escala de conceptos fundacionales. Crucialmente, actúa como un repositorio de datos de alta calidad para entrenar sistemas de IA para la formalización y la demostración de teoremas. Por el contrario, el artículo postula que las herramientas de IA acelerarán el desarrollo de CSLib mismo, creando un "efecto volante" donde los expertos humanos y las herramientas de IA se vuelven progresivamente más eficientes en la producción de conocimiento verificado.

Los autores enfatizan que, si bien las formalizaciones generadas por IA conllevan riesgos de errores o falta de comprensibilidad humana, estos se mitigarán manteniendo un proceso de revisión de código con el humano en el bucle, donde la IA desempeña únicamente un papel consultivo. El objetivo final es democratizar los métodos formales, haciéndolos accesibles para una amplia gama de científicos de la computación, desde teóricos hasta constructores de sistemas.