Saltar al contenido principal
Seguridad y pruebas

Certora Prover

Verificación formal

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

Ver siguiente

Kontrol - formal verification tool based on Foundry and KEVM

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

Etiquetas

  • Verificación formal
  • Verificación
  • Seguridad

RepositorioCertora

Información

Tipo
Verificación formal
Estrellas en GitHub
339
Licencia
GPL-3.0
Listado revisado
septiembre 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.

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.