Saltar al contenido principal
Seguridad y pruebas

Verifereum

Verificación formal

Visitar sitio web (se abre en una pestaña nueva)Verifereum en X (se abre en una pestaña nueva)Verifereum en GitHub (se abre en una pestaña nueva)

Ver siguiente

Certora AutoProver

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

Etiquetas

  • Seguridad
  • Educación
  • Verificación formal

Repositorioverifereum

Información

Tipo
Verificación formal
Estrellas en GitHub
54
Licencia
GPL-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.