Certora Prover

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 es una herramienta para traducciones de alta garantía de un gran subconjunto de Rust a lenguajes formales como F* o Rocq.

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

Certora AutoProver is an AI bot that automates parts of formal verification for smart contracts. Verification engineers use it to generate and run checks with less manual specification work.

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.