Runtime Verification demostró que Algorand no puede bifurcarse — su herramienta KAVM lleva inactiva desde 2023

2026-08-19

formal-verification · security · audits · consensus · kavm · discovery · web · updated

Un teorema de seguridad verificado por máquina

En 2019, el equipo de Algorand entregó su protocolo de consenso a una pequeña startup de Champaign-Urbana y pidió algo que pocas blockchains habían encargado: una prueba verificada por máquina de que el protocolo nunca podría dividirse. Runtime Verification, entonces conocida por aplicar métodos formales a código aeroespacial y automotriz, lo logró usando Coq, un asistente de pruebas interactivo.

La verificación formal funciona de manera distinta a las pruebas. En lugar de ejecutar el código con entradas de muestra y esperar que los casos cubran los caminos peligrosos, el ingeniero escribe el sistema como definiciones matemáticas y luego demuestra propiedades sobre él como un matemático demuestra un teorema, con cada paso de inferencia comprobado por software. La intuición humana puede saltarse un paso o contar mal un caso límite; el asistente de pruebas no.

Esa garantía es la base matemática de la finalidad de un solo bloque de Algorand — la propiedad de que un bloque confirmado es permanente, sin período de espera probabilístico para confirmaciones adicionales. El propio anuncio de Algorand en su momento calificó a la cadena como 'la primera blockchain en ofrecer finalidad inmediata de transacciones'.

El modelo, publicado en junio de 2019 por los investigadores de RV Musab Alturki, Brandon Moore, Karl Palmskog y Lucas Pena, dividió el teorema de seguridad en unos 170 lemas y precisó las suposiciones en las que se basa la garantía, incluida que una supermayoría del stake está en manos de usuarios honestos. El repositorio algorand-verification sigue siendo público, con versiones de mantenimiento hasta 2022. Los expertos en el protocolo de Algorand, Jing Chen, Nickolai Zeldovich y Victor Luchangco, trabajaron junto al equipo de RV en el encargo.

De teoremas de protocolo a un banco de auditorías DeFi

El encargo de 2019 se convirtió en una relación duradera. En julio de 2020, la Fundación Algorand otorgó a RV una subvención dentro de su programa de subvenciones ecosistémicas de 250 millones de ALGO para construir un marco semántico formal para los contratos inteligentes de Algorand utilizando el Framework K, el 'lenguaje de programación para lenguajes de programación' de RV — un sistema que permite a los ingenieros definir el comportamiento de un lenguaje una vez y derivar automáticamente intérpretes, depuradores y herramientas de verificación a partir de esa definición. La propuesta original preveía formalizar un lenguaje de alto nivel adaptado de Clarity de Blockstack; para cuando se lanzó una beta pública en 2023, el trabajo se había centrado en la Máquina Virtual de Algorand (AVM), el motor de ejecución de los contratos inteligentes de Algorand, y en TEAL, el lenguaje ensamblador que interpreta la AVM, que Algorand había lanzado mientras tanto.

En diciembre de 2021, RV anunció que se había convertido en el socio de seguridad de la Fundación. 'Esperamos con interés nuestra colaboración y damos la bienvenida a Runtime Verification Inc como nuestro socio de seguridad', dijo Addie Wagenknecht, entonces directora de Ecosistemas Globales y Operaciones Técnicas de la Fundación. El trabajo de auditoría siguió a gran escala: entre julio de 2021 y diciembre de 2022, RV publicó trece encargos de auditoría que abarcaban la primera ola de aplicaciones DeFi del ecosistema — los AMM, los pools de contratos inteligentes que fijan precios de operaciones mediante fórmulas en lugar de un libro de órdenes, junto con préstamos, liquid staking y stablecoins.

Concepto	Implicación en el mundo real
Tinyman AMM V2 (diciembre de 2022)	El AMM más grande de Algorand recibió una revisión de cinco semanas antes de lanzar flash swaps, préstamos flash y comisiones de pool configurables.
Pact, Pact Router y Pact Stableswap (febrero–agosto de 2022)	Los pools centrales del AMM, su contrato de enrutamiento de múltiples pools y su invariante matemático stableswap fueron auditados por separado.
Algofi Lending v2 (agosto de 2022)	Mercados de préstamos para ALGO y ASA, la stablecoin STBL2 y una bóveda de garantía de gobernanza revisados en un solo encargo.
xBacked (septiembre de 2022)	Las bóvedas maestras y el pool de estabilidad de una stablecoin sobrecolateralizada, auditados en Reach, un lenguaje de contratos inteligentes especializado.
Hone Liquid Staking (septiembre de 2022)	Staking de recompensas de gobernanza que acuña el token líquido dALGO; la auditoría redujo un diseño de dos contratos a uno.
EXA Finance Baskets (mayo de 2022)	Comercio entre pares de cestas de hasta cuatro activos a través de cuatro modelos de intercambio.
Folks Finance, Yieldly, XET y los contratos de recompensas de gobernanza (2021–22)	Préstamos, staking de múltiples tokens, despliegue de tokens y la maquinaria de gobernanza comunitaria de la primera ola.

La metodología fue consistente en todo el banco: los auditores reconstruyeron los invariantes — las propiedades que deben cumplirse para que un sistema sea seguro — a partir de la documentación del protocolo, revisaron el código on-chain línea por línea, y luego simularon grandes cantidades de comportamientos adversos con herramientas internas como pyteal_eval y tstmodel. Donde los contratos estaban escritos en Tealish, RV también revisó la salida TEAL del transpilador para no tener que confiar en el compilador. Bajo la colaboración, RV revisó además StakerDAO y AlgoDex en 2021. El resultado más contundente del lote: la revisión de primera ronda de xBacked reveló cinco hallazgos de alta severidad, uno medio y uno informativo, con una segunda ronda que añadió dos hallazgos medios y otro informativo. En todos los encargos de 2022, el equipo auditado abordó los problemas antes del lanzamiento.

KAVM: el probador que detectó un error de redondeo

El producto de la subvención se hizo público en marzo de 2023 como KAVM — la semántica formal de la Máquina Virtual de Algorand, construida sobre K — presentado como una forma de verificar formalmente contratos inteligentes de Algorand 'sin necesidad de tener un doctorado en Ciencias de la Computación.' KAVM se integró con PyTeal, el framework de Python de Algorand para escribir contratos inteligentes, y con py-algorand-sdk; su tutorial de lanzamiento recorría un contrato K Coin Vault para mostrar lo que la herramienta podía hacer.

La demo es la ilustración más clara de por qué la verificación formal se justifica en la cadena. Los contratos inteligentes calculan con enteros de punto fijo, no con números de punto flotante, por lo que el orden de las operaciones en una expresión aritmética cambia el resultado: X multiplicado por Y y luego dividido por Z no es lo mismo que X dividido por Z y luego multiplicado por Y, una vez que el redondeo interviene. El método de quema de la bóveda dividía por el tipo de cambio antes de escalar — un código que parecía correcto pero que devolvía silenciosamente cero para cantidades pequeñas de quema. El probador de KAVM marcó el método porque la expresión simbólica de su salida no coincidía con la postcondición que el desarrollador había especificado; una suite de pruebas convencional que usara números redondos pasaba el mismo código. Es precisamente la clase de bug — pérdida de fondos de usuarios por aritmética — que la metodología de auditoría de RV incluye entre sus comprobaciones estándar.

Concepto	Implicación en el mundo real
Decoradores @router.precondition y @router.postcondition en métodos ABI de PyTeal	Un desarrollador declara suposiciones y salidas esperadas directamente en el código del contrato; el probador verifica la implementación contra ellas.
Integración de kavm.algod con py-algorand-sdk	Los scripts de despliegue y pruebas existentes pueden ejecutarse contra KAVM como sustituto de un nodo vivo, no solo contra un sandbox.
Integración planificada con AlgoKit	Habría convertido a KAVM en un reemplazo directo del Sandbox de Algorand, llevando la verificación a cualquier proyecto AlgoKit.

Entonces el desarrollo se detuvo. El README de KAVM aún lleva el banner 'Work in progress', lista la prueba simbólica ('kavm prove') como 'Not yet implemented', y advierte que las pruebas de especificación 'no se han portado completamente a la semántica actual y están fallando'. No todos los opcodes de TEAL son compatibles y faltan las llamadas entre contratos. El último commit del repositorio es una actualización rutinaria de dependencias del 2 de agosto de 2023; el repositorio de la demo se tocó por última vez en enero de 2024. KAVM demostró el enfoque en un contrato y nunca se convirtió en la herramienta de desarrollo mantenida y documentada que prometía su publicación de lanzamiento — una beta que se publicó y luego se apagó.

Un nodo de retransmisión para monitoreo en tiempo real

Tres semanas después del último commit de KAVM, RV anunció un tipo diferente de contribución a Algorand: un nodo de retransmisión registrado. Los relés son la columna vertebral de la red — nodos de archivo que mantienen copias completas del libro mayor, validan y reenvían transacciones, y aparecen en los registros DNS SRV de Algorand para que los nodos de participación puedan descubrirlos y conectarse a ellos. En ese momento había alrededor de 110 relés registrados, entre ellos el de RV.

El relé servía a una agenda de monitoreo. El plan de RV era convertir los invariantes demostrados durante las auditorías en monitores en tiempo real que observen los contratos desplegados y puedan disparar transacciones de recuperación cuando una propiedad se rompe — por ejemplo, marcando un préstamo insuficientemente garantizado antes de que dañe un protocolo de préstamos. La mayoría de los servicios de indexación son demasiado lentos para ese trabajo, así que ejecutar un relé dio a RV observación directa y de baja latencia del flujo de transacciones de la red. Si ese relé sigue registrado hoy en día no se pudo verificar: su documentación se movió detrás de un inicio de sesión de GitBook, la Wayback Machine no guarda ninguna instantánea de ella, y el conjunto actual de registros SRV no identifica claramente el nombre de host de RV.

La empresa de la era de la IA — y el conjunto de herramientas Algorand inactivo

Runtime Verification hoy lidera su página principal con 'Software Assurance for the AI Age' y ha reorganizado sus servicios en tres líneas.

Concepto	Implicación en el mundo real
Software Quality Assurance	El negocio principal de auditoría — modelado, identificación de propiedades, fuzzing y verificación formal — para equipos que 'no pueden permitirse fallos de software'.
Data Partnerships	RV ofrece sus años de trabajo de modelado y verificación como datos de entrenamiento para LLMs que aprenden prácticas de ingeniería de alta calidad.
Agentic Guardrails	Aplicación de políticas de seguridad para agentes de IA: saber qué puede hacer un agente, probar que se mantiene dentro de los límites y detectar violaciones.

La empresa es real y está ocupada. Fundada en 2010 a partir de la Universidad de Illinois en Urbana-Champaign, cuenta con más de 25 ingenieros senior, una antigüedad media de 4 años, y un legado con la NASA (tres subvenciones SBIR consecutivas) y Boeing. Su trabajo de exhibición actual es entre cadenas: una revisión previa al lanzamiento de Monad, auditorías de los contratos de staking de Espresso y de la VM Soroban de Stellar, endurecimiento del intérprete WASMI, y verificación formal de los programas de estándar de tokens de Solana. El CEO Everett Hildenbrandt describe el estándar de trabajo sin rodeos: 'Un informe de auditoría de Runtime Verification es un sello de aprobación de nuestro equipo.' Su producto de verificación de contratos inteligentes en desarrollo activo está enfocado en Ethereum: Kontrol, construido sobre la semántica KEVM, tuvo commits tan recientes como agosto de 2026.

El lado de Algorand cuenta una historia diferente. No ha aparecido ninguna publicación etiquetada con Algorand en el blog de RV desde agosto de 2023, y la página dedicada a la colaboración con Algorand que archivaba la cronología completa del encargo ahora redirige a la página de inicio. La comunidad de Algorand no ha olvidado la relación — los hilos del foro desde 2019 han citado repetidamente la prueba de seguridad contra las críticas al protocolo, y una publicación de gobernanza de junio de 2026 que recomendaba una auditoría de terceros mencionaba a Runtime Verification — pero el apetito por la verificación formal de la AVM sobrevivió al desarrollo de KAVM. En mayo de 2023, una propuesta comunitaria (xGov-18) solicitó 250,000 ALGO para terminar una biblioteca de AVM versión 8 basada en Coq, presentada explícitamente como una 'alternativa a la biblioteca semántica de la AVM del Framework K'; la solicitud de incorporación de la propuesta se fusionó en el repositorio de xGov, y la biblioteca en ese momento permitía ejecutar 25 opcodes de la AVM.

Lo que perdura para Algorand es ese teorema de 2019: la prueba verificada por máquina sigue siendo pública y no revocada, y los informes de auditoría de la ola DeFi aún están en el repositorio público de RV. Pero un desarrollador que hoy lance un contrato serio de Algorand debe saber que KAVM no es una opción de verificación mantenida — el camino práctico de garantía es una auditoría convencional, o el razonamiento semi-formal de invariantes que describen las propias guías de desarrollador de Algorand. La brecha entre lo que demostró el encargo de 2019 y lo que finalmente entregó la línea de herramientas es la medida honesta de la relación: una prueba fundacional, un sólido banco de auditorías y una herramienta insignia que nunca llegó a producción.

Fuentes

Source: https://runtimeverification.com/