Verificación formal

Los tests comprueban un contrato frente a los casos que alguien pensó en escribir; la verificación formal intenta cubrirlos todos. Primero se redacta una especificación, un conjunto de propiedades que el código debe respetar siempre, como que la oferta total sea igual a la suma de saldos o que nadie pueda retirar más de lo que depositó. Después, herramientas como solucionadores SMT, motores de ejecución simbólica o asistentes de demostración tratan de probar que esas propiedades se cumplen para cualquier entrada y estado, o devuelven un contraejemplo.

Como los contratos son inmutables y guardan grandes sumas, los protocolos de alto valor recurren cada vez más a ella. El contrato de depósito de la beacon chain de Ethereum se verificó formalmente antes del lanzamiento, y mercados de préstamo, stablecoins y DEX usan probadores especializados para comprobar sus invariantes clave. Los rollups y los circuitos ZK son candidatos naturales, porque su corrección es matemática por definición.

Una demostración vale lo que vale su especificación: si las propiedades no recogen el riesgo real, un código verificado puede seguir siendo explotable, y los supuestos sobre contratos externos, oráculos o el compilador pueden no cumplirse. Es un proceso lento y caro, así que suele reservarse a los componentes críticos y se combina con auditorías, fuzzing y bug bounties en lugar de sustituirlos.