-
Hasta ahora demostró la estructura de transacciones y bloques; el límite de 21 millones, no.
-
Todo el código fue escrito por modelos de IA, pero McClelland asegura haber revisado cada línea.
El ingeniero Keagan McClelland, cofundador de Start9 Labs, presentó este 14 de julio en una entrevista con el sitio educativo The Space «BTC Verified», un nuevo sistema que le permitiría a un software comprobar, con precisión matemática, que el código que aplica las reglas centrales de Bitcoin hace exactamente lo que promete hacer.
Esas reglas (cuánto se puede emitir, o qué cadena de las que compiten es la válida) actualmente las hacen cumplir los nodos que ejecutan un software escrito y revisado por personas. Esa revisión humana, por más rigurosa que sea, no equivale a una demostración matemática de que el código hace lo que se supone que debe hacer, enfatizó Keagan.
BTC Verified propone justamente eso, que un software compruebe, con la misma certeza que se usa para demostrar un teorema matemático, que las reglas del protocolo Bitcoin más importantes se cumplen siempre, sin excepciones.
McClelland no apunta este desarrollo al usuario final de Bitcoin, sino a los programadores que mantienen el software de la red y a quienes construyen versiones alternativas de ese mismo software (Bitcoin Core, Knots, entre otros). Si dos implementaciones distintas logran demostrar matemáticamente que cumplen las mismas reglas, cualquier persona podría correr la que prefiera con la misma confianza.
Para el usuario común, el impacto sería indirecto, ya que el objetivo es reducir el riesgo de errores que sí lo afectan de lleno. McClelland recordó, en la entrevista, la vez en que Bitcoin sufrió una división accidental de cadena al cambiar de una base de datos por otra, en 2013.
El error de Keagan que disparó BTC Verified y la verificación matemática
McClelland contó en la entrevista que su interés por este tipo de certeza nace de una frustración personal. Al comienzo de su carrera como programador, escribió una línea de código en el lenguaje C++ que usaba paréntesis en lugar de corchetes para reservar espacio en la memoria de la computadora. Ese error, mínimo a la vista, le provocó una falla conocida como error de segmentación (segmentation fault), un tipo de falla que no da ninguna pista sobre su causa. Tardó dos días en encontrarla.
Esa experiencia lo llevó a buscar lenguajes de programación que impidieran escribir, directamente, código que no tenga sentido. Lean 4 es uno de esos lenguajes, según él mismo. Se trata de un asistente de pruebas, un programa construido sobre tipos dependientes (un sistema que permite expresar reglas matemáticas muy precisas dentro del propio código) y que verifica demostraciones matemáticas de forma automática, sin margen para el error humano en esa verificación.
Con esa herramienta, McClelland ya logró demostrar que la forma en que Bitcoin codifica sus transacciones y bloques no admite ambigüedades, y que la raíz de Merkle (el resumen criptográfico que identifica a todas las transacciones de un bloque) corresponde siempre a un único conjunto de datos, según el repositorio del proyecto.
Por otro lado, todo el código detrás de BTC Verified fue escrito por modelos de inteligencia artificial, incluidos Claude y Codex, según indicó McClelland en la entrevista. El ingeniero aclaró que revisó personalmente cada línea y guio las decisiones del desarrollo, aunque no fue quien escribió el código letra por letra.
McClelland encuadra su propio trabajo dentro de una idea que él mismo bautizó como «Formal Vibefication» (algo así como una improvisación formalizada), según la cual los modelos de inteligencia artificial actuales vuelven asequible ese tipo de certeza matemática para muchos más proyectos de software.
Lo que McClelland reconoce que todavía falta
Demostrar que Bitcoin nunca emitirá más de 21 millones de unidades, o que la red siempre elige como válida la cadena con más trabajo acumulado, es lo más difícil del proyecto y todavía no está resuelto.
Ambas demostraciones se apoyan en una equivalencia formal entre programas informáticos y demostraciones matemáticas, conocida como isomorfismo de Curry-Howard. Bajo esa equivalencia, una afirmación lógica (por ejemplo, que nunca habrá más de 21 millones de bitcoins) puede traducirse en un programa, y ese programa, si existe y compila sin errores, funcionaría como la prueba de que la afirmación es cierta. McClelland fijó como meta informal terminar la prueba sobre la elección de cadena «antes de que termine el verano» boreal, aunque aclaró que se trata de un cálculo conservador.
El propio McClelland reconoce, en la publicación donde presentó el proyecto en el foro para desarrolladores Delving Bitcoin, que su trabajo «es estructuralmente incapaz» de garantizar cómo se comporta en la práctica el software Bitcoin Core, la implementación de referencia que ejecuta la mayoría de los nodos de la red.
Si el enfoque avanza, McClelland cree que podría ayudar a resolver discusiones técnicas que hoy dividen a la comunidad de Bitcoin, como el diseño de BIP-360, la propuesta que busca proteger a la red de un futuro ataque de una computadora cuántica. El propio McClelland, sin embargo, describe a BTC Verified como un trabajo sin fecha de cierre, que seguirá creciendo a medida que más partes del protocolo se sometan a este tipo de prueba matemática.
