Saltar al contenido principal
Seguridad y pruebas

K Semantics of the Ethereum Virtual Machine (EVM)

Verificación formal

Ver en GitHub (se abre en una pestaña nueva)K Semantics of the Ethereum Virtual Machine (EVM) en X (se abre en una pestaña nueva)

Ver siguiente

hax

Acerca de K Semantics of the Ethereum Virtual Machine (EVM)

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.

Etiquetas

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

Repositorioruntimeverification

Información

Tipo
Verificación formal
Estrellas en GitHub
595
Licencia
BSD-3-Clause
Listado revisado
junio de 2026

Herramientas similares

Certora Prover

Certora Prover

Certora Prover is a cloud formal-verification service that checks specifications written in CVL against deployed contract code. Verification engineers use it to prove that a contract holds stated properties for all inputs.

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.

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.