Zum Hauptinhalt springen
Kontrol - formal verification tool based on Foundry and KEVM
Security & testing

Kontrol - formal verification tool based on Foundry and KEVM

Formal verification

Foundry · Bildung · Governance · Formale Verifikation · Solidity · Laufzeitverifikation · Vertragsbereitstellung · Statische Analyse

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

Kontrol hebt Foundry-Eigenschaftstests in KEVM-gestützte Beweise, sodass Sie formale Garantien mit weniger handgeschriebener Spezifikationsarbeit als mit reinem KEVM allein anstreben können.

Related resources

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM ist die ausführbare K-Framework-Semantik der EVM: Wenden Sie sie auf Bytecode an, wenn Sie konformitätsgeprüfte Ausführung, symbolische Erkundung, Gas-Analysen oder Beweise benötigen, die den Regeln von Ethereum genau folgen.

hax

hax ist ein Tool für hochsichere Übersetzungen einer großen Teilmenge von Rust in formale Sprachen wie F* oder Rocq.

Act

Act

Act ist Ethereums deklarative Spezifikationssprache und Toolchain zur Beschreibung aller Verhaltensweisen eines EVM-Programms, sodass SMT-Solver, Theorembeweiser oder wirtschaftliche Analysetools über die Korrektheit auf Bytecode-Ebene und die Anreizkompatibilität nachdenken können, einschließlich automatischer Verfeinerungsbeweise gegen konkrete Implementierungen.

Verifereum

Verifereum

Verifereum verbindet Ethereum-Smart-Contracts mit HOL4-gestütztem Theorembeweisen, sodass Sie sehr starke Korrektheitsansprüche anstreben können, wenn automatisierte SMT-Ansätze nicht ausreichen.