Lean verificó el código y el fuzzer halló el bug

Lean verificó el código. El fuzzer encontró el bug de todas formas

Lean 4 demostró matemáticamente que lean-zip, una implementación verificada de zlib, era correcta. Semanas después, un fuzzer encontró un desbordamiento de búfer en el runtime de Lean y una vulnerabilidad de denegación de servicio en el parser ZIP — ambos componentes que la verificación formal nunca llegó a cubrir. Para cualquier founder que haya apostado por software verificado como escudo de seguridad, este caso es una llamada de atención urgente.

El experimento, documentado por Kiran en su blog técnico, combina dos disciplinas que normalmente viven en silos: la verificación formal y el fuzzing. El resultado pone sobre la mesa una pregunta incómoda: ¿quién vigila a los que vigilan?

¿Qué es la verificación formal con Lean 4 y por qué la están usando startups?

La verificación formal consiste en demostrar matemáticamente que un programa cumple una especificación dada. No es simplemente escribir tests — es probar, con la misma rigurosidad de un teorema matemático, que el código no puede comportarse de formas no deseadas.

👥 ¿Quieres ir más allá de la noticia?

En nuestra comunidad discutimos las tendencias, compartimos oportunidades y nos ayudamos entre emprendedores. Sin humo, solo acción.

👥 Unirme a la comunidad

Lean 4 es uno de los asistentes de prueba interactivos más avanzados del momento. Permite escribir código funcional y al mismo tiempo demostrar propiedades sobre ese código usando tipos dependientes. En los últimos años ha ganado tracción en academia y en equipos de ingeniería que construyen infraestructura crítica.

El proyecto lean-zip es precisamente ese tipo de apuesta: una implementación del descompresor deflate (el algoritmo detrás de zlib y ZIP) escrita en Lean y verificada formalmente. El objetivo era tener una librería cuya lógica de descompresión fuera matemáticamente correcta — sin bugs lógicos, sin comportamientos indefinidos en el código de aplicación.

Y en ese objetivo, Lean cumplió: el código de la aplicación estaba libre de errores críticos. La verificación funcionó exactamente como se supone que debe funcionar.

¿Dónde apareció el bug si el código estaba verificado?

Aquí está el insight central del caso: la verificación formal solo cubre lo que tú decides verificar. El problema no estaba en el descompresor — estaba en la base de confianza (trusted computing base) sobre la que corre ese código verificado.

El fuzzer reveló dos vulnerabilidades distintas:

Desbordamiento de búfer (buffer overflow) en el runtime de Lean, escrito en C. Lean compila a código nativo usando un runtime propio — y ese runtime, a diferencia del código de la aplicación, no estaba verificado formalmente.
Vulnerabilidad de denegación de servicio (DoS) en el parser de archivos ZIP. El parser que maneja la estructura del archivo ZIP era un componente separado, no cubierto por las pruebas formales. Con entradas ZIP malformadas, colapsaba el proceso.

La lección es directa: verificaste la parte que programaste, pero tu código corre sobre un runtime, un sistema operativo, librerías de terceros — ninguno de los cuales estaba dentro del perímetro de la verificación.

Verificación formal vs. fuzzing: no son enemigos, son complementarios

El error conceptual más frecuente en equipos de ingeniería es tratar la verificación formal y el fuzzing como alternativas. No lo son — son herramientas que atacan tipos de problemas distintos.

Verificación formal:

Garantiza corrección para las propiedades que especificas
Exhaustiva dentro de su modelo — si lo demuestra, es verdad
No puede cubrir lo que no modelas explícitamente
Costosa en tiempo de ingeniería; escala mal en sistemas grandes

Fuzzing (AFL++, libFuzzer):

Genera miles de entradas malformadas automáticamente
Descubre bugs empíricos en código real en ejecución — incluyendo runtimes y parsers
No es exhaustivo: puede no encontrar un bug en millones de intentos
Rápido de integrar en pipelines de CI/CD

El stack ideal combina ambos: verificación formal para la lógica crítica del producto, fuzzing para la integración con runtimes, parsers y librerías externas. El caso lean-zip es la demostración práctica de por qué necesitas los dos.

Este problema no es nuevo: seL4, CompCert y la trampa de la base de confianza

Lean-zip no es el primer proyecto verificado que encuentra bugs fuera del perímetro formal. Este patrón tiene nombre en la comunidad de seguridad: el problema de la Trusted Computing Base (TCB).

seL4, el microkernel verificado formalmente más conocido del mundo, tiene propiedades de seguridad matemáticamente probadas — pero esas pruebas asumen que el hardware funciona correctamente, que el compilador no introduce errores y que los drivers externos son confiables. Ninguna de esas asunciones está dentro de la verificación.

CompCert, el compilador C verificado de INRIA, es otro caso ilustrativo: la lógica del compilador está probada, pero bugs en código cliente o en optimizaciones no cubiertas por las pruebas formales han generado problemas en integración real.

El patrón es consistente: cuanto más sofisticado es el sistema, más capas hay fuera del modelo formal. Y cada capa no verificada es un vector de ataque potencial.

¿Qué significa esto para tu startup?

Si estás construyendo software donde la seguridad importa — fintech, healthtech, infraestructura crítica, herramientas con IA — este caso tiene implicaciones directas para tus decisiones de ingeniería.

Primero, la verificación formal no es una bala de plata. Que Lean (o Coq, o Isabelle) haya demostrado que tu código es correcto no significa que tu sistema sea seguro. Significa que tu código de aplicación cumple las propiedades que especificaste. Tu runtime, tu parser, tus dependencias de C — eso está fuera.

Segundo, el fuzzing es asequible y debería estar en tu pipeline hoy. Herramientas como AFL++ o libFuzzer no requieren equipos especializados para empezar. Google mantiene OSS-Fuzz, un servicio gratuito de fuzzing continuo para proyectos open-source que encuentra más de 800 bugs por año en librerías ampliamente usadas. Si tienes una librería open-source, puedes integrarte a OSS-Fuzz en horas.

Tercero, mapea tu base de confianza antes de hacer promesas de seguridad. Antes de decirle a un cliente o inversor que tu sistema es seguro porque está verificado formalmente, responde: ¿qué runtime usa ese código? ¿Qué librerías externas toca? ¿Qué parsers procesa datos del usuario? Todo lo que no está en tu modelo formal es un punto ciego.

Acciones concretas que puedes implementar esta semana:

Integra fuzzing en tu CI/CD: Añade AFL++ o libFuzzer a tu pipeline de integración continua. Empieza por los componentes que procesan entradas del usuario — APIs, parsers de archivos, formularios.
Documenta tu TCB: Crea un inventario explícito de todos los componentes que tu código verificado asume como correctos: runtime del lenguaje, librerías del sistema, dependencias de terceros. Ese documento es tu mapa de riesgo real.
Combina herramientas según el riesgo: En lógica de negocio crítica (cálculo de intereses, procesamiento de pagos, reglas de compliance), vale la inversión en especificación formal. En parsers e integraciones, el fuzzing es más eficiente para el ROI que obtienes.
Evalúa OSS-Fuzz si tienes código open-source: Si parte de tu stack es open-source, integrar OSS-Fuzz es gratuito y puede descubrir vulnerabilidades antes de que lo haga un atacante.

La perspectiva para el ecosistema hispano: una oportunidad de diferenciación

En LATAM y España, el mercado de software seguro está creciendo impulsado por regulación (GDPR en Europa, nuevas leyes de datos en México, Brasil y Colombia) y por la expansión del fintech y el healthtech. Sin embargo, la brecha en prácticas de seguridad avanzada sigue siendo amplia.

Según datos de S3lab (Universidad de Deusto), una fracción significativa de equipos de desarrollo en la región implementan verificación parcial sin complementarla con fuzzing sobre runtimes — exactamente el escenario que este caso expone como peligroso.

Para una startup hispana que quiere competir en mercados regulados o vender a empresas grandes, implementar una estrategia híbrida (verificación formal + fuzzing) no es solo una buena práctica de ingeniería — es un argumento de venta diferenciador. Los compradores enterprise en Europa y Norteamérica valoran cada vez más la evidencia de seguridad proactiva, no solo los certificados.

Conclusión

Lean demostró que lean-zip era correcto. Y lo era — en las partes que se modelaron formalmente. El bug apareció en el runtime de C y en el parser ZIP, dos componentes que nunca entraron al modelo.

El caso no debilita el valor de la verificación formal — lo refuerza, precisamente porque muestra dónde tiene y dónde no tiene alcance. La ingeniería de seguridad robusta no elige entre verificación formal y fuzzing: usa ambas donde cada una tiene más impacto, con una comprensión explícita de qué está dentro y qué está fuera de la base de confianza.

La pregunta que todo founder tech debería hacerse no es «¿está verificado mi código?» sino «¿qué asume mi verificación que es correcto y nunca comprobé?». La respuesta a esa pregunta define tu superficie de ataque real.