Glossary
Verificación formal
Probar matemáticamente — no solo testear — que un contrato inteligente satisface una especificación precisa, usando herramientas como Certora, K o asistentes de prueba.
La verificación formal sustituye el testing por la demostración. El ingeniero escribe una especificación ("la oferta total es igual a la suma de los balances", "ningún caller puede drenar más que su balance") y una herramienta de verificación o bien prueba que la spec se cumple para todas las entradas posibles, o bien produce un contraejemplo.
Herramientas como Certora Prover, Halmos, KEVM y asistentes de prueba dedicados (Coq, Lean, Isabelle) se usan en los contratos más críticos para la seguridad: Maker, Aave, Compound, Lido. El coste es elevado — escribir la spec correctamente es un esfuerzo de ingeniería propio — pero para contratos de miles de millones de dólares es cada vez más el estándar.