El bug de SQLite que duró 16 años

SQLite suele venderse como una pieza pequeña, confiable y aburrida. Y justo por eso sorprende más cuando aparece una falla que se quedó viva durante 16 años. No estamos hablando de un bug cualquiera en una app de escritorio o de una web con poco tráfico. Hablamos de un problema en el modo WAL de SQLite, una parte usada para mejorar concurrencia y persistencia, que logró pasar desapercibida durante años hasta que alguien la atacó con verificación formal.

La historia, contada por Canonical en su blog, mezcla ingeniería de bases de datos, modelos matemáticos y una pregunta muy práctica: ¿cómo encuentras errores que sobreviven tanto tiempo en software que millones de personas usan sin pensar? La respuesta corta es TLA+. La larga vale la pena, porque te muestra por qué la verificación formal no es teoría académica para decorar slides, sino una herramienta útil cuando el costo de un bug es alto. Fuente: Ubuntu Blog y la documentación oficial de TLA+ y SQLite WAL.

Qué pasó con SQLite y el modo WAL

SQLite tiene una reputación fuerte por una razón simple: funciona bien en muchísimos escenarios, desde apps móviles hasta sistemas embebidos. Su modo WAL, o Write-Ahead Logging, permite que lecturas y escrituras convivan mejor que en el modo tradicional de rollback journal. En lugar de reescribir la base principal en cada cambio, SQLite va registrando las modificaciones en un archivo WAL y después las consolida.

El problema es que WAL no es solo una optimización. También introduce reglas de consistencia, checkpoints, lectura de snapshots y una coordinación precisa entre procesos. Cuando esas reglas tienen una esquina mal modelada, el sistema puede comportarse de forma incorrecta solo bajo ciertas secuencias de eventos. Por eso un bug así puede vivir 16 años: no aparece en el camino feliz, no rompe pruebas triviales y, en producción, quizá solo se manifiesta con cargas raras o timing específico.

Por qué un bug puede durar tanto

Hay tres razones muy concretas. Primero, el espacio de estados es enorme: no basta con probar “leer, escribir, cerrar”. Tienes que considerar interleavings, reinicios, checkpoints, archivos parcialmente escritos y lectores que llegan tarde. Segundo, muchas pruebas unitarias validan comportamiento visible, no invariantes internas. Tercero, si el bug ocurre en una secuencia poco común, nadie lo ve hasta que una herramienta lo busca de forma sistemática.

En software crítico, esa combinación es peligrosa. Piensa en bases de datos embebidas en routers, dispositivos industriales, sistemas de sincronización o servicios que usan SQLite como almacenamiento local. Un error raro puede no ser masivo, pero sí suficiente para corromper datos, perder transacciones o dejar una aplicación en un estado inconsistente.

WAL en una frase

WAL funciona como un cuaderno de cambios antes de actualizar el libro principal. Eso mejora concurrencia, pero también obliga a respetar reglas precisas sobre qué se puede leer, cuándo se puede limpiar el registro y qué pasa si el sistema se interrumpe a mitad de camino. Si una de esas reglas falla, el bug puede esconderse durante años.

Cómo entra TLA+ en esta historia

TLA+ es un lenguaje para especificar sistemas concurrentes y distribuidos de forma matemática. No sirve para reemplazar tests, sino para responder una pregunta distinta: ¿tu diseño permite estados inválidos? En vez de ejecutar el programa, modelas su comportamiento y le pides al verificador que explore todas las rutas posibles dentro del modelo.

Eso cambia el juego porque los bugs de concurrencia no suelen depender de una sola línea mal escrita. Dependen de secuencias. TLA+ te deja expresar estados, acciones e invariantes. Si el modelo encuentra una ruta que viola la propiedad que querías preservar, te devuelve un contraejemplo. Y ese contraejemplo suele ser mucho más útil que un crash report de producción, porque muestra la cadena exacta de pasos que rompe la lógica.

La documentación oficial de TLA+ explica justamente esa idea: especificar lo que el sistema debe cumplir y luego verificarlo con herramientas como TLC. No necesitas modelar cada detalle de implementación para obtener valor. A veces basta con capturar la estructura lógica del protocolo o del subsistema que te preocupa.

Qué modelas y qué no modelas

No modelas todo el código fuente. Modelas la parte relevante del comportamiento. En el caso de SQLite WAL, eso significa representar estados del archivo WAL, lectores, checkpoints y condiciones de avance. El objetivo no es simular bytes exactos del disco, sino encontrar una secuencia de acciones que deje al sistema en un estado imposible o inconsistente.

Eso es importante porque mucha gente cree que verificación formal significa hacer el modelo tan grande como el sistema real. No. El valor está en abstraer bien. Si abstraes mal, no encuentras nada. Si abstraes bien, puedes descubrir una falla que pasó 16 años sin que nadie la viera.

Qué tipo de bug detecta mejor

TLA+ brilla en problemas como estos:

1. Protocolos con varios actores concurrentes.
2. Estados que dependen de orden de eventos.
3. Invariantes que deben mantenerse siempre.
4. Sistemas donde un caso raro puede ser peor que un fallo obvio.

SQLite WAL encaja perfecto. Hay múltiples actores, estados temporales y reglas que deben sostenerse incluso si el proceso se corta, se reinicia o compite con otro lector.

El bug histórico: qué clase de error era

No hace falta convertir esto en una autopsia de código para entender la lección. El punto central es que el bug estaba ligado a la semántica del WAL y a cómo se manejaban ciertos estados durante la lectura y el checkpoint. En otras palabras, no era un typo ni una condición obvia, sino una falla de diseño o de coordinación que solo aparece bajo combinaciones específicas.

Ese tipo de error es justo el que las pruebas convencionales suelen dejar pasar. Un test normal ejecuta un caso, quizá diez. TLA+ explora muchas más combinaciones. Ahí está la diferencia entre probar y verificar ciertas propiedades del sistema.

Para aterrizarlo, imagina que tienes este conjunto de eventos:

El bug aparece cuando una secuencia concreta rompe una suposición interna. Si no recorres esa secuencia exacta, todo parece normal.

Por qué esto importa fuera de SQLite

Si usas bases de datos embebidas, colas locales, caches persistentes o cualquier mecanismo con estado y concurrencia, el patrón se repite. El problema no es solo si el código corre. El problema es si todas las rutas posibles preservan la propiedad que te importa: no perder datos, no duplicar eventos, no leer estados inválidos.

En Latinoamérica esto importa más de lo que parece. Muchas empresas operan con infraestructura ajustada, conectividad irregular y equipos pequeños. Un bug raro en una base local puede traducirse en horas de soporte, datos inconsistentes o procesos manuales para reparar registros. No siempre necesitas una falla masiva para tener un problema serio.

Qué aprendemos sobre verificación formal

La lección más útil no es “usa TLA+ en todo”. La lección es saber dónde vale la pena. Si el sistema tiene estados concurrentes, invariantes importantes y costo alto de fallo, la verificación formal deja de ser opcional y pasa a ser una inversión razonable.

TLA+ no reemplaza pruebas, observabilidad ni revisión de código. Las complementa. Las pruebas te dicen que algo funciona en los casos que ejecutaste. TLA+ te ayuda a descubrir si existe algún camino lógico que rompa tu propiedad, aunque nunca hayas pensado en ese camino.

Ventajas concretas frente a pruebas tradicionales

• Encuentra secuencias raras sin que tengas que adivinarlas.
• Expone contraejemplos legibles, no solo fallos genéricos.
• Obliga a escribir invariantes de forma explícita.
• Sirve para revisar decisiones de diseño antes de implementar.
• Reduce el riesgo en componentes donde un error cuesta más que el tiempo invertido en modelar.

Limitaciones que conviene asumir

TLA+ no es magia. Si modelas mal, puedes dejar fuera justo el caso que te importa. Si el sistema cambia mucho, el modelo también necesita mantenimiento. Y si tu equipo nunca trabajó con especificaciones formales, hay una curva de aprendizaje real.

Aun así, el retorno puede ser alto. Encontrar un bug de 16 años en un componente tan usado demuestra que el modelo sí puede ver cosas que el código y los tests no ven. Eso no significa que debas formalizar todo el stack. Significa que cuando el riesgo lo justifica, vale la pena.

Cómo aplicar esta idea en tu equipo

Si trabajas en producto, infraestructura o backend, no necesitas empezar con un modelo gigante. Empieza por un subsistema pequeño pero crítico. Un protocolo de locking, una cola de eventos, una máquina de estados de pagos o una lógica de replicación son buenos candidatos.

Una forma práctica de arrancar es esta:

1. Elige una propiedad que no puedes romper, por ejemplo, “nunca perder una transacción confirmada”.
2. Dibuja los estados posibles del sistema en papel.
3. Identifica acciones: leer, escribir, reintentar, reiniciar, consolidar.
4. Define invariantes, no solo casos felices.
5. Modela la versión mínima en TLA+.
6. Corre TLC y revisa contraejemplos.
7. Ajusta el diseño antes de tocar producción.

Si tu equipo ya usa pruebas de integración o chaos engineering, TLA+ encaja como una capa previa. Te ayuda a filtrar errores lógicos antes de gastar tiempo en reproducciones complejas.

Cuándo sí vale la pena invertir

Hay señales claras. Si el bug más caro de tu sistema es raro pero catastrófico, si dependes de concurrencia o si tu equipo ya perdió tiempo persiguiendo estados imposibles, la verificación formal empieza a pagar sola. También sirve cuando quieres documentar un protocolo de forma precisa y evitar que el conocimiento quede solo en la cabeza de una persona.

Cuándo no es la mejor herramienta

Si estás construyendo una landing page, una app de contenido o un CRUD simple sin estados complicados, probablemente no necesitas TLA+. Ahí te convienen más tests, linting, observabilidad y buenas prácticas de arquitectura. La clave es no convertir una herramienta especializada en religión.

Qué dice esto sobre el software que usamos todos los días

La parte más incómoda de esta historia es que el bug no estaba en un proyecto experimental. Estaba en SQLite, una pieza muy madura y muy confiable. Eso te recuerda que la antigüedad del software no garantiza ausencia de fallos, solo significa que una parte del problema ya fue explorada.

También te deja una idea útil para equipos en Ecuador y en toda LatAm: no siempre necesitas más código, sino mejores garantías sobre el código que ya tienes. Si tu sistema maneja pagos, inventario, mensajería, sincronización offline o datos sensibles, un bug raro puede costarte mucho más que unas horas de modelado.

La verificación formal no sustituye a la ingeniería práctica. Pero cuando se usa bien, te da algo valioso: confianza basada en estados posibles, no solo en la suerte de que tus tests no hayan fallado todavía.

Tabla resumen

Si quieres quedarte con una sola idea, que sea esta: los bugs más caros no siempre son los más visibles. A veces sobreviven porque solo aparecen en combinaciones raras de estados. Ahí es donde TLA+ deja de ser una curiosidad académica y se vuelve una herramienta útil para ingeniería real.