Security & testing

Kontrol - formal verification tool based on Foundry and KEVM

Formal verification

Foundry · Educación · Gobernanza · Verificación formal · Solidity · Verificación en tiempo de ejecución · Despliegue de contratos · Análisis estático

Social runtimeverification/kontrol(118 ☆)runtimeverification/optimism-ci(4 ☆)runtimeverification/_audits_lidofinance_dual-governance_fork(1 ☆)runtimeverification/yearn-v3-term-vault(0 ☆)runtimeverification/Depeg-swap(0 ☆)runtimeverification/_audits_Ethereum-optimism_pausability(0 ☆)

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.

Related resources

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

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.

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.