hax

La KEVM es la semántica ejecutable del marco K de la EVM: apúntela al código de bytes cuando necesite una ejecución con comprobación de conformidad, exploración simbólica, razonamiento de gas o pruebas que sigan de cerca las reglas de Ethereum.

Kontrol eleva las pruebas de propiedades de Foundry a pruebas respaldadas por la KEVM para que pueda buscar garantías formales con menos trabajo de especificación escrito a mano que la KEVM sin procesar por sí sola.

Act es el lenguaje de especificación declarativa y la cadena de herramientas de Ethereum para describir todos los comportamientos de un programa de la EVM, de modo que los solucionadores SMT, los demostradores de teoremas o las herramientas de análisis económico puedan razonar sobre la corrección a nivel de código de bytes y la compatibilidad de incentivos, incluyendo pruebas de refinamiento automático frente a implementaciones concretas.

Verifereum conecta los contratos inteligentes de Ethereum con la demostración de teoremas respaldada por HOL4 para que pueda apuntar a afirmaciones de corrección muy sólidas cuando los enfoques SMT automatizados no son suficientes.