Los tests comprueban un contrato frente a los casos que alguien pens\u00f3 en escribir; la verificaci\u00f3n formal intenta cubrirlos todos. Primero se redacta una especificaci\u00f3n, un conjunto de propiedades que el c\u00f3digo debe respetar siempre, como que la oferta total sea igual a la suma de saldos o que nadie pueda retirar m\u00e1s de lo que deposit\u00f3. Despu\u00e9s, herramientas como solucionadores SMT, motores de ejecuci\u00f3n simb\u00f3lica o asistentes de demostraci\u00f3n tratan de probar que esas propiedades se cumplen para cualquier entrada y estado, o devuelven un contraejemplo.<\/p>\n
Como los contratos son inmutables y guardan grandes sumas, los protocolos de alto valor recurren cada vez m\u00e1s a ella. El contrato de dep\u00f3sito de la beacon chain de Ethereum se verific\u00f3 formalmente antes del lanzamiento, y mercados de pr\u00e9stamo, stablecoins y DEX usan probadores especializados para comprobar sus invariantes clave. Los rollups y los circuitos ZK son candidatos naturales, porque su correcci\u00f3n es matem\u00e1tica por definici\u00f3n.<\/p>\n
Una demostraci\u00f3n vale lo que vale su especificaci\u00f3n: si las propiedades no recogen el riesgo real, un c\u00f3digo verificado puede seguir siendo explotable, y los supuestos sobre contratos externos, or\u00e1culos o el compilador pueden no cumplirse. Es un proceso lento y caro, as\u00ed que suele reservarse a los componentes cr\u00edticos y se combina con auditor\u00edas, fuzzing y bug bounties en lugar de sustituirlos.<\/p>\n","protected":false},"excerpt":{"rendered":"
La verificaci\u00f3n formal usa pruebas matem\u00e1ticas y herramientas autom\u00e1ticas para demostrar que el c\u00f3digo de un contrato cumple su especificaci\u00f3n en todo caso.<\/p>\n","protected":false},"template":"","meta":{"footnotes":""},"class_list":["post-182244","ce_glossary","type-ce_glossary","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/crypto-economy.com\/es\/wp-json\/wp\/v2\/ce_glossary\/182244","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/crypto-economy.com\/es\/wp-json\/wp\/v2\/ce_glossary"}],"about":[{"href":"https:\/\/crypto-economy.com\/es\/wp-json\/wp\/v2\/types\/ce_glossary"}],"version-history":[{"count":0,"href":"https:\/\/crypto-economy.com\/es\/wp-json\/wp\/v2\/ce_glossary\/182244\/revisions"}],"wp:attachment":[{"href":"https:\/\/crypto-economy.com\/es\/wp-json\/wp\/v2\/media?parent=182244"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}