Saltar al contenido principal
Seguridad y pruebas

Act

Verificación formal

Ver en GitHub (se abre en una pestaña nueva)

Ver siguiente

Verifereum

Acerca de 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.

Etiquetas

  • Educación
  • Análisis
  • Verificación formal
  • Ejecución simbólica

Repositorioethereum

Información

Tipo
Verificación formal
Estrellas en GitHub
284
Licencia
AGPL-3.0
Listado revisado
junio de 2026

Herramientas similares

K Semantics of the Ethereum Virtual Machine (EVM)

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.

hax

hax

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

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.