Saltar al contenido principal
K Semantics of the Ethereum Virtual Machine (EVM)
Security & testing

K Semantics of the Ethereum Virtual Machine (EVM)

Formal verification

Seguridad · Educación · Análisis · Verificación formal · Ejecución simbólica · Herramientas de depuración · Verificación en tiempo de ejecución · Vyper

Social (opens in a new tab)runtimeverification/evm-semantics(586 ☆) (opens in a new tab)

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.

Related resources

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol - formal verification tool based on Foundry and KEVM

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.

hax

hax es una herramienta para traducciones de alta garantía de un gran subconjunto de Rust a lenguajes formales como F* o Rocq.

Act

Act

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

Verifereum

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.