Zum Hauptinhalt springen
Verifereum
Security & testing

Verifereum

Formal verification

Sicherheit · Bildung · Formale Verifikation

Website (opens in a new tab)Social (opens in a new tab)verifereum/verifereum(51 ☆) (opens in a new tab)

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.

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.

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol - formal verification tool based on Foundry and KEVM

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.

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.