El 25 de junio de 2026, el equipo de Ubuntu publicó discretamente un artículo técnico en su blog. El titular encerraba dos hechos aparentemente contradictorios: SQLite —la base de datos más utilizada del planeta— tenía un bug. Y ese bug llevaba en el código desde 2010.
Dicho de otro modo: llevaba 16 años escondido.
¿Qué son 16 años? En 2010 acababa de salir el iPhone 4, WeChat ni existía, y la gente todavía mandaba SMS con teclado numérico. Ese mismo año, una línea de código introdujo el fallo en SQLite. Desde entonces, el bug ha vivido plácidamente dentro de cada teléfono inteligente, cada navegador y cada sistema operativo. Cientos de millones de dispositivos. Dieciséis años. Y jamás nadie lo detectó.
Al final, quien lo encontró no fue una persona: fue un problema de matemáticas.
Modelo TLA+ del comportamiento del checkpoint WAL de SQLite creado por el equipo de Ubuntu. Bastan 20 pasos para reproducir el bug oculto durante 16 años. Fuente: ubuntu.com
Empecemos por el principio: qué es SQLite y por qué está en tu móvil
Aclaremos una cosa: SQLite no es una «aplicación». En tu teléfono no hay un icono que ponga «SQLite». Es un «motor de base de datos»: un software especializado en almacenar y gestionar datos dentro de teléfonos, ordenadores y navegadores.
Unos ejemplos: el historial de chats de WhatsApp, los contactos de tu agenda, las contraseñas que guarda el navegador, los datos locales que generan apps como Amazon, TikTok o tu banco… detrás de prácticamente todo eso está SQLite, funcionando en silencio. Es la base de datos con mayor despliegue del mundo, sin discusión. Se estima que hay más de un billón de bases de datos SQLite activas en el planeta.
Que un software de este calibre —un auténtico cimiento sobre el que se asienta medio mundo digital— haya albergado un bug durante 16 años ya es, de por sí, para ponerse los pelos de punta.
Pero lo realmente fascinante de esta historia es cómo se encontró.
Un fallo imposible de detectar por un ser humano
Veamos primero el bug en sí. SQLite tiene un modo de funcionamiento llamado WAL (Write-Ahead Log, o registro de escritura anticipada). Simplificando mucho: cuando varios programas leen y escriben la base de datos a la vez, el WAL actúa como un «cuaderno de borrador». Quien escribe lo hace primero en el borrador, los que leen no se ven afectados de momento, y cuando se termina de escribir, el contenido se traspasa al «libro oficial». Este proceso se llama checkpoint.
El fallo aparece justo cuando la acción de «traspasar» y la de «escribir» coinciden en el tiempo. Pongamos un ejemplo cotidiano:
Imagina que tú y un compañero manipuláis simultáneamente una hoja de cálculo. Tu compañero está añadiendo datos nuevos en la «zona de borrador», mientras que a ti te toca pasar al archivo oficial lo que ya está confirmado en el borrador. Echáis un vistazo al borrador, veis que hay 100 registros pendientes de traspaso, y empiezas a copiar. Cuando llevas 50, tu compañero mete 5 registros más y reinicia el contador del borrador. Tú sigues copiando los 50 que te quedan, pero como el contador se ha reiniciado, en realidad solo estás copiando números antiguos: te saltas los datos que de verdad había que mover.
Resultado: al archivo oficial le faltan unos cuantos registros. Datos perdidos.
Esto es exactamente lo que describe la documentación oficial de SQLite: una «condición de carrera» (race condition) durante el checkpoint del WAL. Dos operaciones que no se han coordinado correctamente colisionan en una ventana de tiempo increíblemente precisa.
La clave está en esas dos palabras: «increíblemente precisa». Para que el bug se active tienen que darse a la vez un montón de condiciones muy concretas: la escritura y el checkpoint deben ocurrir simultáneamente; justo después de que el checkpoint lea el tamaño del WAL pero antes de que empiece a copiar, otra operación de escritura tiene que completarse y resetear el WAL. Esa ventana temporal puede ser de apenas unos microsegundos.
Cuando un humano escribe casos de prueba para encontrar bugs, lo que hace en el fondo es «conjeturar»: imagina dónde podría haber un problema y lanza intentos en esa dirección. Pero la ventana que dispara este bug es tan estrecha que resulta imposible de «adivinar». Da igual cuántos testers contrates o cuántos scripts de testing automatizado escribas: nunca vas a poder cubrir todas las combinaciones posibles de orden de operaciones, porque el número de combinaciones es astronómico.
Por eso este bug ha podido dormir tan tranquilo durante 16 años dentro de cientos de millones de dispositivos.
Qué es TLA+: no es una herramienta de testing, es una demostración matemática
Para entender cómo el equipo de Ubuntu encontró el fallo, conviene entender antes un concepto: la verificación formal.
Usemos la analogía más simple posible: el testing tradicional es como un «control aleatorio»: metes la mano en un saco de arroz, coges unos cuantos granos y miras si hay arena. La verificación formal es como una «demostración matemática»: puedes deducir lógicamente si hay o no arena en el saco, sin necesidad de revisar grano por grano.
TLA+ es una herramienta de verificación formal. Las siglas significan Temporal Logic of Actions (Lógica Temporal de Acciones). La inventó Leslie Lamport, una leyenda de la informática que también creó LaTeX (el sistema de composición de documentos académicos) y diseñó el algoritmo de consenso Paxos, sobre el que se asienta prácticamente cualquier sistema distribuido actual.
Lo que hace TLA+ es, en esencia, lo siguiente: describes el comportamiento del software que quieres comprobar mediante un modelo matemático abstracto —no necesitas escribir código, solo expresar en lenguaje matemático «cómo debería cambiar esto según las distintas circunstancias»—. Después, el comprobador de modelos de TLA+ explora de forma exhaustiva todas las combinaciones de estados posibles para verificar si las reglas que has definido se cumplen siempre.
En palabras del equipo de Ubuntu: después de construir el modelo TLA+ del comportamiento del WAL de SQLite, el comprobador de modelos «encontró un contraejemplo en solo 20 pasos». Veinte pasos. Dieciséis años frente a veinte pasos.
Versión estática del modelo TLA+: muestra cómo la condición de carrera entre las operaciones de escritura y checkpoint provoca pérdida de datos. Fuente: ubuntu.com
Por qué el ojo humano jamás podrá ganar esta batalla
Aquí se abre una cuestión profunda que merece la pena desarrollar: ¿cómo es posible que un método matemático encuentre algo que ha permanecido invisible durante 16 años? La respuesta está en una diferencia metodológica de raíz.
Los métodos humanos de prueba —ya sea haciendo clics manualmente o escribiendo scripts automatizados— son, en esencia, «enumerativos»: elaboras una lista de escenarios que crees que podrían fallar y los verificas uno a uno. El problema es que el espacio de estados de un sistema software sufre una explosión combinatoria. En un sistema con 100 pasos de operación, las ordenaciones posibles de estados son del orden de 100 factorial: una cifra mayor que el número de átomos del universo. Resulta físicamente imposible enumerarlas todas.
En cambio, una herramienta de verificación formal como TLA+, aunque también se enfrenta en teoría al problema de la «explosión de estados», es capaz de algo que ningún humano puede hacer: comprobar si, dentro de todas las condiciones que yo he definido, puede llegar a aparecer un problema.
Conviene rumiar esta frase dos veces.
El testing humano responde a la pregunta: «¿Qué problemas he visto?». La verificación formal responde a la pregunta: «¿Existe la posibilidad de que haya un problema?».
Lo primero es pasivo, depende de la imaginación y deja escapar cosas con facilidad. Lo segundo es activo, exhaustivo, y no se le escapa ninguno de los estados que ha calculado.
Los ingenieros de Ubuntu no son más listos que los desarrolladores de SQLite —el equipo de SQLite es famoso por la calidad estratosférica de su código y la cobertura de pruebas está entre las más altas del sector—. La diferencia está en la herramienta. Con una regla y con un microscopio no se ve el mismo mundo.
Un hallazgo inesperado: por qué a la competencia no le afectó
La historia trae un epílogo interesante. Si el equipo de Ubuntu se puso a hacer esta verificación fue porque ellos mismos mantienen un proyecto llamado Dqlite: una base de datos distribuida construida sobre SQLite. La pregunta que se hicieron fue: ¿este bug de SQLite también afecta a Dqlite?
Así que construyeron otro modelo TLA+, esta vez de Dqlite. ¿Resultado? Dqlite no está afectado.
El motivo es sencillo: Dqlite tiene un diseño más «conservador». Cuando ejecuta un checkpoint, bloquea por completo la operación de escritura, garantizando que «traspasar» y «escribir» no puedan coincidir en el tiempo. Esto penaliza un poco el rendimiento, pero de rebote sortea limpiamente la condición de carrera.
No es que el diseño de Dqlite sea mejor. Pero a veces una decisión conservadora que tomaste sin darle mayor importancia acaba demostrando, dieciséis años después, que era la decisión correcta. Las cadenas causales de la ingeniería de software son así de curiosas.
El parche de SQLite: una sola línea de código
El 5 de marzo de 2026, SQLite publicó oficialmente la corrección. El arreglo es mínimamente simple: durante el checkpoint se añade una comprobación extra para verificar que el WAL no ha sido reseteado. Si lo ha sido, se reinicia el proceso.
Traducido: dieciséis años de riesgo latente, resueltos con una línea de código.
Pero que el código sea simple no significa que el problema lo fuera. Dar con el sitio exacto donde había que poner esa línea y decidir qué condición debía comprobar es un proceso endiabladamente difícil. Tan difícil que los ingenieros de SQLite —algunas de las personas que más saben de bases de datos en el mundo— no lo vieron en dieciséis años.
Qué significa todo esto: una tendencia que está cambiando las reglas
Dos reflexiones para cerrar.
La primera: el caso de SQLite no es una excepción. Amazon, Microsoft, Oracle y otras empresas ya usan TLA+ desde hace años para verificar infraestructuras críticas. Servicios fundamentales de AWS como S3 o DynamoDB pasaron por el comprobador de modelos de TLA+ en sus fases tempranas de diseño. Lo que pasa es que la mayoría de esos casos ocurren de puertas adentro, en sistemas cerrados, y el público no los ve. SQLite, como proyecto open source omnipresente, es el primer caso de altísima visibilidad pública en el que un bug se descubre mediante verificación formal. Y eso lo convierte en un hito.
La segunda: el «umbral de entrada» de la verificación formal está bajando. TLA+ no es una herramienta para todo el mundo: requiere mentalidad matemática y capacidad de modelado de sistemas. Pero igual que hace veinte años nadie pensaba que el «testing automatizado» fuese algo que todo el mundo debiera hacer y hoy es un estándar, la verificación formal está pasando de «cosa de genios» a «estándar de equipo». Que el equipo de Ubuntu haya encontrado con TLA+ un bug en la base de datos más madura y extendida del sector es un dato que habla por sí solo: las infraestructuras de software que damos por sentadas pueden esconder fallos que ni siquiera sus propios autores conocen. Y las matemáticas son el único camino fiable para encontrarlos.
Hace 16 años, el software se probaba con intuición y mucha dedicación. 16 años después, un problema matemático ha encontrado en 20 pasos un fallo que el ojo humano jamás habría visto.
No es que los ingenieros sean mejores. Es que las herramientas han mejorado.
Enlaces de referencia: